(Joint Center)Library stripped_odd_order_theorem

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Prelude ssreflect ssrbool ssrfun eqtype ssrnat fintype finset fingroup.
Require morphism quotient action gfunctor gproduct commutator gseries nilpotent.
Require PFsection14.

This file contains a minimal, self-contained reformulation of the Odd Order theorem, using only the bare Coq logic, and avoiding any use of extra-logical features such as notation, coercion or implicit arguments. This stripped theorem would hardly be usable, however; it just provides evidence for the sceptics.
Equivalence and equality

Inductive equivalent P Q := Equivalent (P_to_Q : PQ) (Q_to_P : QP).

Inductive equal T (x : T) : TType := Equal : equal T x x.

Arithmetic

Inductive natural := Zero | Add_1_to (n : natural).

Fixpoint add (m n : natural) : natural :=
  match m with Zeron | Add_1_to m_minus_1add m_minus_1 (Add_1_to n) end.

Definition double (n : natural) : natural := add n n.

Inductive odd (n : natural) :=
  Odd (half : natural)
    (n_odd : equal natural n (Add_1_to (double half))).

Inductive less_than (m n : natural) :=
  LessThan (diff : natural)
    (m_lt_n : equal natural n (Add_1_to (add m diff))).

Finite subsets

Definition injective_in T R (D : TType) (f : TR) :=
   x y, D xD yequal R (f x) (f y) → equal T x y.

Inductive in_image T R (D : TType) (f : TR) (a : R) :=
  InImage (x : T) (x_in_D : D x) (a_is_fx : equal R a (f x)).

Inductive finite_of_order T (D : TType) (n : natural) :=
  FiniteOfOrder (rank : Tnatural)
    (rank_injective : injective_in T natural D rank)
    (rank_onto :
        i, equivalent (less_than i n) (in_image T natural D rank i)).

Elementary group theory

Inductive group_axioms T (mul : TTT) (one : T) (inv : TT) :=
  GroupAxioms
    (associativity : x y z, equal T (mul x (mul y z)) (mul (mul x y) z))
    (left_identity : x, equal T (mul one x) x)
    (left_inverse : x, equal T (mul (inv x) x) one).

Inductive group T mul one inv (G : TType) :=
  Group
    (G_closed_under_mul : x y, G xG yG (mul x y))
    (one_in_G : G one)
    (G_closed_under_inv : x, G xG (inv x)).

Inductive subgroup T mul one inv (H G : TType) :=
  Subgroup
    (H_group : group T mul one inv H)
    (H_subset_G : x, H xG x).

Inductive normal_subgroup T mul one inv (H G : TType) :=
  NormalSubgroup
    (H_subgroup_G : subgroup T mul one inv H G)
    (H_is_G_invariant : x y, H xG yH (mul (inv y) (mul x y))).

Inductive commute_mod T mul (x y : T) (H : TType) :=
  CommuteMod (z : T)
    (z_in_H : H z)
    (xy_eq_zyx : equal T (mul x y) (mul z (mul y x))).

Inductive abelian_factor T mul one inv (G H : TType) :=
  AbelianFactor
    (G_group : group T mul one inv G)
    (H_normal_in_G : normal_subgroup T mul one inv H G)
    (G_on_H_abelian : x y, G xG ycommute_mod T mul x y H).

Inductive solvable_group T mul one inv (G : TType) :=
| TrivialGroupSolvable
   (G_trivial : x, equivalent (G x) (equal T x one))
| AbelianExtensionSolvable (H : TType)
   (H_solvable : solvable_group T mul one inv H)
   (G_on_H_abelian : abelian_factor T mul one inv G H).


The Odd Order theorem

Theorem stripped_Odd_Order T mul one inv (G : TType) (n : natural) :
    group_axioms T mul one invgroup T mul one inv G
    finite_of_order T G nodd n
  solvable_group T mul one inv G.