Remove coqprime-8.4

We're using tactics in terms in some places, and so have no hope of
compiling with Coq 8.4.  We no longer pretend to support it.

We can probably also remove some other compatibility things, if we want.

1 files changed, 0 insertions, 605 deletions

diff --git a/coqprime-8.4/Coqprime/EGroup.v b/coqprime-8.4/Coqprime/EGroup.v
deleted file mode 100644
index 553cb746c..000000000
--- a/coqprime-8.4/Coqprime/EGroup.v
+++ /dev/null
@@ -1,605 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-(**********************************************************************
-    EGroup.v                                
-                                                                     
-    Given an element a, create the group {e, a, a^2, ..., a^n}
- **********************************************************************)
-Require Import Coq.ZArith.ZArith.
-Require Import Coqprime.Tactic.
-Require Import Coq.Lists.List.
-Require Import Coqprime.ZCAux.
-Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
-Require Import Coq.Arith.Wf_nat.
-Require Import Coqprime.UList.
-Require Import Coqprime.FGroup.
-Require Import Coqprime.Lagrange.
-
-Open Scope Z_scope.
-
-Section EGroup.
-
-Variable A: Set.
-
-Variable A_dec: forall a b: A, {a = b} + {~ a = b}.
-
-Variable op: A -> A -> A.
-
-Variable a: A.
-
-Variable G: FGroup op.
-
-Hypothesis a_in_G: In a G.(s).
-
-
-(************************************** 
-  The power function for the group
- **************************************)
- 
-Set Implicit Arguments.
-Definition gpow n := match n with  Zpos p => iter_pos p _ (op a) G.(e)  | _ => G.(e) end.
-Unset Implicit Arguments.
-
-Theorem gpow_0: gpow 0 = G.(e).
-simpl; sauto.
-Qed.
-
-Theorem gpow_1 : gpow 1 = a.
-simpl; sauto.
-Qed.
-
-(************************************** 
-  Some properties of the power function
- **************************************)
- 
-Theorem gpow_in: forall n, In (gpow n) G.(s).
-intros n; case n; simpl; auto.
-intros p; apply iter_pos_invariant with (Inv := fun x => In x G.(s)); auto.
-Qed.
-
-Theorem gpow_op: forall b p, In b G.(s) -> iter_pos p _ (op a) b = op (iter_pos p _ (op a) G.(e)) b.
-intros b p; generalize b; elim p; simpl; auto; clear  b p.
-intros p Rec b Hb.
-assert (H: In (gpow (Zpos p)) G.(s)).
-apply gpow_in.
-rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos p A x y)); auto.
-repeat rewrite G.(assoc); auto.
-intros p Rec b Hb.
-assert (H: In (gpow (Zpos p)) G.(s)).
-apply gpow_in.
-rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos p A x y)); auto.
-repeat rewrite G.(assoc); auto.
-intros b H; rewrite e_is_zero_r; auto.
-Qed.
-
-Theorem gpow_add: forall n m, 0 <= n -> 0 <= m -> gpow (n + m) = op (gpow n) (gpow m).
-intros n; case n.
-intros m _ _; simpl; apply sym_equal; apply e_is_zero_l; apply gpow_in.
-2: intros p m H; contradict H; auto with zarith.
-intros p1 m; case m.
-intros _ _; simpl; apply sym_equal; apply e_is_zero_r.
-exact (gpow_in (Zpos p1)).
-2: intros p2 _ H; contradict H; auto with zarith.
-intros p2 _ _; simpl.
-rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos p2 A x y)); auto.
-exact (gpow_in (Zpos p2)).
-Qed.
-
-Theorem gpow_1_more: 
-  forall n, 0 < n -> gpow n = G.(e) -> forall m, 0 <= m -> exists p, 0 <= p < n /\ gpow m = gpow p.
-intros n H1 H2 m Hm;  generalize Hm; pattern m; apply Z_lt_induction; auto with zarith; clear m Hm.
-intros m Rec Hm.
-case (Zle_or_lt n m); intros H3.
-case (Rec (m - n)); auto with zarith.
-intros p (H4,H5); exists p; split; auto.
-replace m with (n + (m - n)); auto with zarith.
-rewrite gpow_add; try rewrite H2; try rewrite H5; sauto; auto with zarith.
-generalize gpow_in; sauto.
-exists m; auto.
-Qed.
-
-Theorem gpow_i: forall n m, 0 <= n -> 0 <= m -> gpow n = gpow (n + m) -> gpow m = G.(e).
-intros n m H1 H2 H3; generalize gpow_in; intro PI.
-apply g_cancel_l with (g:= G) (a := gpow n); sauto.
-rewrite <- gpow_add; try rewrite <- H3; sauto.
-Qed.
-
-(************************************** 
-  We build the support by iterating the power function
- **************************************)
-
-Set Implicit Arguments.
-
-Fixpoint support_aux (b: A) (n: nat) {struct n}: list A :=
-b::let c := op a b in
-    match n with 
-       O => nil | 
-      (S n1) =>if A_dec c G.(e) then nil else  support_aux c n1 
-    end.
-
-Definition support := support_aux G.(e) (Zabs_nat (g_order G)).
-
-Unset Implicit Arguments.
-
-(************************************** 
-  Some properties of the support that helps to prove that we have a group
- **************************************)
-
-Theorem support_aux_gpow: 
-  forall n m b, 0 <=  m -> In b (support_aux (gpow m) n) -> 
-        exists p, (0 <= p < length (support_aux (gpow m) n))%nat  /\ b = gpow (m + Z_of_nat p).
-intros n; elim n; simpl.
-intros n1 b Hm [H1 | H1]; exists 0%nat; simpl; rewrite Zplus_0_r; auto; case H1.
-intros n1 Rec m b Hm [H1 | H1].
-exists 0%nat; simpl; rewrite Zplus_0_r; auto; auto with arith.
-generalize H1; case (A_dec (op a (gpow m)) G.(e)); clear H1; simpl; intros H1 H2.
-case H2.
-case (Rec (1 + m) b); auto with zarith.
-rewrite gpow_add; auto with zarith.
-rewrite gpow_1; auto.
-intros p (Hp1, Hp2); exists (S p); split; auto with zarith. 
-rewrite <- gpow_1.
-rewrite <- gpow_add; auto with zarith.
-rewrite inj_S; rewrite Hp2; eq_tac; auto with zarith.
-Qed.
-
-Theorem gpow_support_aux_not_e: 
-  forall n m p, 0 <= m -> m < p < m + Z_of_nat (length (support_aux (gpow m) n)) -> gpow p <> G.(e).
-intros n; elim n; simpl.
-intros m p Hm (H1, H2); contradict H2; auto with zarith.
-intros n1 Rec m p Hm; case (A_dec (op a (gpow m)) G.(e)); simpl.
-intros _ (H1, H2); contradict H2; auto with zarith.
-assert (tmp: forall p, Zpos (P_of_succ_nat p) = 1 + Z_of_nat p).
-intros p1; apply trans_equal with (Z_of_nat (S p1)); auto; rewrite inj_S; auto with zarith.
-rewrite tmp.
-intros H1 (H2, H3); case (Zle_lt_or_eq (1 + m) p); auto with zarith; intros H4; subst.
-apply (Rec (1 + m)); try split; auto with zarith.
-rewrite gpow_add; auto with zarith.
-rewrite gpow_1; auto with zarith.
-rewrite gpow_add; try rewrite gpow_1; auto with zarith.
-Qed.
-
-Theorem support_aux_not_e: forall n m b, 0 <= m -> In b (tail (support_aux (gpow m) n)) -> ~ b = G.(e).
-intros n; elim n; simpl.
-intros m b Hm H; case H.
-intros n1 Rec m b Hm; case (A_dec (op a (gpow m)) G.(e)); intros H1 H2; simpl; auto.
-assert (Hm1: 0 <= 1 + m); auto with zarith.
-generalize( Rec (1 + m) b Hm1) H2; case n1; auto; clear Hm1.
-intros _ [H3 | H3]; auto.
-contradict H1; subst; auto.
-rewrite gpow_add; simpl; try rewrite e_is_zero_r; auto with zarith.
-intros n2; case (A_dec (op a (op a (gpow m))) G.(e)); intros H3.
-intros _ [H4 | H4].
-contradict H1; subst; auto.
-case H4.
-intros H4 [H5 | H5]; subst; auto.
-Qed.
-
-Theorem support_aux_length_le: forall n a, (length (support_aux a n) <= n + 1)%nat.
-intros n; elim n; simpl; auto.
-intros n1 Rec a1; case (A_dec (op a a1) G.(e)); simpl; auto with arith.
-Qed.
-
-Theorem support_aux_length_le_is_e: 
-   forall n m, 0 <= m ->  (length (support_aux (gpow m) n) <= n)%nat -> 
-      gpow (m + Z_of_nat (length (support_aux (gpow m) n))) = G.(e) .
-intros n; elim n; simpl; auto.
-intros m _ H1; contradict H1; auto with arith.
-intros n1 Rec m Hm; case (A_dec (op a (gpow m)) G.(e)); simpl;  intros H1.
-intros H2; rewrite Zplus_comm; rewrite gpow_add; simpl; try rewrite e_is_zero_r; auto with zarith.
-assert (tmp: forall p, Zpos (P_of_succ_nat p) = 1 + Z_of_nat p).
-intros p1; apply trans_equal with (Z_of_nat (S p1)); auto; rewrite inj_S; auto with zarith.
-rewrite tmp; clear tmp.
-rewrite <- gpow_1.
-rewrite <- gpow_add; auto with zarith.
-rewrite  Zplus_assoc; rewrite (Zplus_comm 1); intros H2; apply Rec; auto with zarith.
-Qed.
-
-Theorem support_aux_in: 
-  forall n m p, 0 <= m ->  (p < length (support_aux (gpow m) n))% nat ->  
-            (In (gpow (m + Z_of_nat p)) (support_aux (gpow m) n)).
-intros n; elim n; simpl; auto; clear n.
-intros m p Hm H1; replace p with 0%nat.
-left; eq_tac; auto with zarith.
-generalize H1; case p; simpl; auto with arith.
-intros n H2; contradict H2; apply le_not_lt; auto with arith.
-intros n1 Rec m p Hm; case (A_dec (op a (gpow m)) G.(e)); simpl; intros H1 H2; auto.
-replace p with 0%nat.
-left; eq_tac; auto with zarith.
-generalize H2; case p; simpl; auto with arith.
-intros n H3; contradict H3; apply le_not_lt; auto with arith.
-generalize H2; case p; simpl; clear H2.
-rewrite Zplus_0_r; auto.
-intros n.
-assert (tmp: forall p, Zpos (P_of_succ_nat p) = 1 + Z_of_nat p).
-intros p1; apply trans_equal with (Z_of_nat (S p1)); auto; rewrite inj_S; auto with zarith.
-rewrite tmp; clear tmp.
-rewrite <- gpow_1; rewrite <- gpow_add; auto with zarith.
-rewrite  Zplus_assoc; rewrite (Zplus_comm 1); intros H2; right; apply Rec; auto with zarith.
-Qed.
-
-Theorem support_aux_ulist: 
-  forall n m, 0 <= m -> (forall p, 0 <= p < m -> gpow (1 + p) <> G.(e)) -> ulist (support_aux (gpow m) n).
-intros n; elim n; auto; clear n.
-intros m _ _; auto.
-simpl; apply ulist_cons; auto.
-intros n1 Rec m Hm H.
-simpl; case (A_dec (op a (gpow m)) G.(e)); auto.
-intros He; apply ulist_cons; auto.
-intros H1; case  (support_aux_gpow n1 (1 + m) (gpow m)); auto with zarith.
-rewrite gpow_add; try rewrite gpow_1; auto with zarith.
-intros p (Hp1, Hp2).
-assert (H2: gpow (1 + Z_of_nat p) = G.(e)).
-apply gpow_i with m; auto with zarith.
-rewrite Hp2; eq_tac; auto with zarith.
-case (Zle_or_lt m  (Z_of_nat p)); intros H3; auto.
-2: case (H (Z_of_nat p)); auto with zarith.
-case (support_aux_not_e (S n1) m (gpow (1 + Z_of_nat p))); auto.
-rewrite gpow_add; auto with zarith; simpl; rewrite e_is_zero_r; auto.
-case (A_dec (op a (gpow m)) G.(e)); auto.
-intros _; rewrite <- gpow_1; repeat rewrite <- gpow_add; auto with zarith.
-replace (1 + Z_of_nat p) with ((1 + m) + (Z_of_nat (p - Zabs_nat m))); auto with zarith.
-apply support_aux_in; auto with zarith.
-rewrite inj_minus1; auto with zarith.
-rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-apply inj_le_rev.
-rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-rewrite <- gpow_1; repeat rewrite <- gpow_add; auto with zarith.
-apply (Rec (1 + m)); auto with zarith.
-intros p H1; case (Zle_lt_or_eq p m); intros; subst; auto with zarith.
-rewrite  gpow_add; auto with zarith.
-rewrite gpow_1; auto.
-Qed.
-
-Theorem support_gpow: forall b, (In b support) -> exists p, 0 <= p < Z_of_nat (length support) /\ b = gpow p.
-intros b H; case (support_aux_gpow  (Zabs_nat (g_order G)) 0 b); auto with zarith.
-intros p ((H1, H2), H3); exists (Z_of_nat p); repeat split; auto with zarith.
-apply inj_lt; auto.
-Qed.
-
-Theorem support_incl_G: incl support G.(s).
-intros a1 H; case (support_gpow a1); auto; intros p (H1, H2); subst; apply gpow_in.
-Qed.
-
-Theorem gpow_support_not_e: forall p, 0 < p < Z_of_nat (length support) -> gpow p <> G.(e).
-intros p (H1, H2); apply gpow_support_aux_not_e with (m := 0) (n := length G.(s)); simpl;
-  try split; auto with zarith.
-rewrite  <- (Zabs_nat_Z_of_nat (length G.(s))); auto.
-Qed.
-
-Theorem support_not_e: forall b, In b (tail support) -> ~ b = G.(e).
-intros b H; apply (support_aux_not_e (Zabs_nat (g_order G)) 0); auto with zarith.
-Qed.
-
-Theorem support_ulist:  ulist support.
-apply (support_aux_ulist (Zabs_nat (g_order G)) 0); auto with zarith.
-Qed.
-
-Theorem support_in_e:  In G.(e) support.
-unfold support; case (Zabs_nat (g_order G)); simpl; auto with zarith.
-Qed.
-
-Theorem gpow_length_support_is_e: gpow (Z_of_nat (length support)) = G.(e).
-apply (support_aux_length_le_is_e (Zabs_nat (g_order G)) 0); simpl; auto with zarith.
-unfold g_order; rewrite Zabs_nat_Z_of_nat; apply ulist_incl_length.
-rewrite  <- (Zabs_nat_Z_of_nat (length G.(s))); auto.
-exact support_ulist.
-rewrite  <- (Zabs_nat_Z_of_nat (length G.(s))); auto.
-exact support_incl_G.
-Qed.
-
-Theorem support_in:  forall p, 0 <= p < Z_of_nat (length support) ->  In (gpow p) support.
-intros p (H, H1); unfold support.
-rewrite <-  (Zabs_eq p); auto with zarith.
-rewrite <-  (inj_Zabs_nat p); auto.
-generalize (support_aux_in (Zabs_nat (g_order G)) 0); simpl; intros H2; apply H2; auto with zarith.
-rewrite <-  (fun x => Zabs_nat_Z_of_nat (@length A x)); auto.
-apply Zabs_nat_lt; split; auto.
-Qed.
-
-Theorem support_internal: forall a b, In a support -> In b support -> In (op a b) support.
-intros a1 b1 H1 H2.
-case support_gpow with (1 := H1); auto; intros p1 ((H3, H4), H5); subst.
-case support_gpow with (1 := H2); auto; intros p2 ((H5, H6), H7); subst.
-rewrite <- gpow_add; auto with zarith.
-case gpow_1_more with (m:= p1 + p2)   (2 := gpow_length_support_is_e); auto with zarith.
-intros p3 ((H8, H9), H10); rewrite H10; apply support_in; auto with zarith.
-Qed.
-
-Theorem support_i_internal: forall a, In a support -> In (G.(i) a) support.
-generalize gpow_in; intros Hp.
-intros a1 H1.
-case support_gpow with (1 := H1); auto.
-intros p1 ((H2, H3), H4); case Zle_lt_or_eq with (1 := H2); clear H2; intros H2; subst.
-2: rewrite gpow_0; rewrite i_e; apply support_in_e.
-replace (G.(i) (gpow p1)) with (gpow (Z_of_nat (length support - Zabs_nat p1))).
-apply support_in; auto with zarith.
-rewrite inj_minus1.
-rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-apply inj_le_rev; rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-apply g_cancel_l with (g:= G) (a := gpow p1); sauto.
-rewrite <- gpow_add; auto with zarith.
-replace (p1 + Z_of_nat (length support - Zabs_nat p1)) with (Z_of_nat (length support)).
-rewrite gpow_length_support_is_e; sauto.
-rewrite inj_minus1; auto with zarith.
-rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-apply inj_le_rev; rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-Qed.
-
-(************************************** 
-  We are now ready to build the group
- **************************************)
-
-Definition Gsupport: (FGroup op).
-generalize support_incl_G; unfold incl; intros Ho.
-apply mkGroup with support G.(e) G.(i); sauto. 
-apply support_ulist.
-apply support_internal.
-intros a1 b1 c1 H1 H2 H3; apply G.(assoc); sauto.
-apply support_in_e.
-apply support_i_internal.
-Defined.
-
-(************************************** 
-  Definition of the order of an element
- **************************************)
-Set Implicit Arguments.
-
-Definition e_order := Z_of_nat (length support).
-
-Unset Implicit Arguments.
-
-(************************************** 
- Some properties of the order of an element
- **************************************)
-
-Theorem gpow_e_order_is_e: gpow e_order = G.(e).
-apply (support_aux_length_le_is_e (Zabs_nat (g_order G)) 0); simpl; auto with zarith.
-unfold g_order; rewrite Zabs_nat_Z_of_nat; apply ulist_incl_length.
-rewrite  <- (Zabs_nat_Z_of_nat (length G.(s))); auto.
-exact support_ulist.
-rewrite  <- (Zabs_nat_Z_of_nat (length G.(s))); auto.
-exact support_incl_G.
-Qed.
-
-Theorem gpow_e_order_lt_is_not_e: forall n, 1 <= n < e_order -> gpow n <> G.(e).
-intros n (H1, H2); apply gpow_support_not_e; auto with zarith.
-Qed.
-
-Theorem e_order_divide_g_order:  (e_order | g_order G).
-change ((g_order Gsupport) | g_order G).
-apply lagrange; auto.
-exact support_incl_G.
-Qed.
-
-Theorem e_order_pos: 0 < e_order.
-unfold e_order, support; case (Zabs_nat (g_order G)); simpl; auto with zarith.
-Qed.
-
-Theorem e_order_divide_gpow: forall n, 0 <= n -> gpow n = G.(e) -> (e_order | n).
-generalize gpow_in; intros Hp.
-generalize e_order_pos; intros Hp1.
-intros n Hn; generalize Hn; pattern n; apply Z_lt_induction; auto; clear n Hn.
-intros n Rec Hn H.
-case (Zle_or_lt  e_order n); intros H1.
-case (Rec (n - e_order)); auto with zarith.
-apply g_cancel_l with (g:= G) (a := gpow e_order); sauto.
-rewrite G.(e_is_zero_r); auto with zarith.
-rewrite <- gpow_add; try (rewrite gpow_e_order_is_e; rewrite <- H; eq_tac); auto with zarith.
-intros k Hk; exists (1 + k).
-rewrite Zmult_plus_distr_l; rewrite <- Hk; auto with zarith.
-case (Zle_lt_or_eq 0 n); auto with arith; intros H2; subst.
-contradict H; apply support_not_e.
-generalize H1; unfold e_order, support.
-case (Zabs_nat (g_order G)); simpl; auto.
-intros H3; contradict H3; auto with zarith.
-intros n1; case (A_dec (op a G.(e)) G.(e)); simpl; intros _ H3.
-contradict H3; auto with zarith.
-generalize H3; clear H3.
-assert (tmp: forall p, Zpos (P_of_succ_nat p) = 1 + Z_of_nat p).
-intros p1; apply trans_equal with (Z_of_nat (S p1)); auto; rewrite inj_S; auto with zarith.
-rewrite tmp; clear tmp; intros H3.
-change (In (gpow n) (support_aux (gpow 1) n1)).
-replace n with (1 + Z_of_nat (Zabs_nat n - 1)).
-apply support_aux_in; auto with zarith.
-rewrite <- (fun x => Zabs_nat_Z_of_nat (@length A x)).
-replace (Zabs_nat n - 1)%nat  with (Zabs_nat (n - 1)).
-apply Zabs_nat_lt; split; auto with zarith.
-rewrite G.(e_is_zero_r) in H3; try rewrite gpow_1; auto with zarith.
-apply inj_eq_rev; rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-rewrite inj_minus1; auto with zarith.
-rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-apply inj_le_rev; rewrite inj_Zabs_nat; simpl; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-rewrite inj_minus1; auto with zarith.
-rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-rewrite Zplus_comm; simpl; auto with zarith.
-apply inj_le_rev; rewrite inj_Zabs_nat; simpl; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-exists 0; auto with arith.
-Qed.
-
-End EGroup.
-
-Theorem gpow_gpow: forall (A : Set) (op : A -> A -> A) (a : A) (G : FGroup op),
-       In a (s G) -> forall n m, 0 <= n -> 0 <= m -> gpow a G (n * m ) = gpow (gpow a G n) G m.
-intros A op a G H n m; case n.
-simpl; intros _ H1; generalize H1.
-pattern m; apply natlike_ind; simpl; auto.
-intros x H2 Rec _; unfold Zsucc; rewrite gpow_add; simpl; auto with zarith.
-repeat rewrite G.(e_is_zero_r); auto with zarith.
-apply gpow_in; sauto.
-intros p1 _; case m; simpl; auto.
-assert(H1: In (iter_pos p1 A (op a) (e G)) (s G)).
-refine (gpow_in _ _ _ _ _ (Zpos p1)); auto.
-intros p2 _;  pattern p2; apply Pind; simpl; auto.
-rewrite Pmult_1_r; rewrite G.(e_is_zero_r); try rewrite G.(e_is_zero_r); auto.
-intros p3 Rec; rewrite Pplus_one_succ_r; rewrite Pmult_plus_distr_l.
-rewrite Pmult_1_r.
-simpl; repeat rewrite iter_pos_plus; simpl.
-rewrite G.(e_is_zero_r); auto.
-rewrite gpow_op with (G:= G); try rewrite Rec; auto.
-apply sym_equal; apply gpow_op; auto.
-intros p Hp; contradict Hp; auto with zarith.
-Qed.
-
-Theorem gpow_e: forall (A : Set) (op : A -> A -> A) (G : FGroup op) n, 0 <= n -> gpow G.(e) G n = G.(e).
-intros A op G n; case n; simpl; auto with zarith.
-intros p _; elim p; simpl; auto; intros p1 Rec; repeat rewrite Rec; auto.
-Qed.
-
-Theorem gpow_pow: forall (A : Set) (op : A -> A -> A) (a : A) (G : FGroup op),
-       In a (s G) -> forall n, 0 <= n -> gpow a G (2 ^ n) = G.(e) -> forall m, n <= m -> gpow a G (2 ^ m) = G.(e).
-intros A op a G H n H1 H2 m Hm.
-replace m with (n + (m - n)); auto with zarith.
-rewrite Zpower_exp; auto with zarith.
-rewrite gpow_gpow; auto with zarith.
-rewrite H2; apply gpow_e.
-apply Zpower_ge_0; auto with zarith.
-Qed.
-
-Theorem gpow_mult: forall (A : Set) (op : A -> A -> A) (a b: A) (G : FGroup op)
-       (comm: forall a b,  In a (s G) -> In b (s G) -> op a b = op b a), 
-       In a (s G) -> In b (s G) -> forall n, 0 <= n -> gpow (op a b) G n = op (gpow a G n) (gpow b G n).
-intros A op a  b G comm Ha Hb n; case n; simpl; auto.
-intros _; rewrite G.(e_is_zero_r); auto.
-2: intros p Hp; contradict Hp; auto with zarith.
-intros p _; pattern p; apply Pind; simpl; auto.
-repeat rewrite G.(e_is_zero_r); auto.
-intros p3 Rec; rewrite Pplus_one_succ_r.
-repeat rewrite iter_pos_plus; simpl.
-repeat rewrite (fun x y H z => gpow_op A  op x G H (op y z)) ; auto.
-rewrite Rec.
-repeat rewrite G.(e_is_zero_r); auto.
-assert(H1: In (iter_pos p3 A (op a) (e G)) (s G)).
-refine (gpow_in _ _ _ _ _ (Zpos p3)); auto.
-assert(H2: In (iter_pos p3 A (op b) (e G)) (s G)).
-refine (gpow_in _ _ _ _ _ (Zpos p3)); auto.
-repeat rewrite <- G.(assoc); try eq_tac; auto.
-rewrite (fun x y => comm (iter_pos p3 A x y) b); auto.
-rewrite (G.(assoc) a); try apply comm; auto.
-Qed.
-
-Theorem Zdivide_mult_rel_prime:  forall a b c : Z, (a | c) -> (b | c) -> rel_prime a b -> (a * b | c).
-intros a b c (q1, H1) (q2, H2) H3.
-assert (H4: (a | q2)).
-apply Gauss with (2 := H3).
-exists q1; rewrite <- H1; rewrite H2; auto with zarith.
-case H4; intros q3 H5; exists q3; rewrite H2; rewrite H5; auto with zarith.
-Qed.
-
-Theorem order_mult: forall (A : Set) (op : A -> A -> A) (A_dec: forall a b: A, {a = b} + {~ a = b}) (G : FGroup op)
-       (comm: forall a b,  In a (s G) -> In b (s G) -> op a b = op b a) (a b: A), 
-       In a (s G) -> In b (s G) -> rel_prime (e_order A_dec a G) (e_order A_dec b G) -> 
-        e_order A_dec (op a b) G = e_order A_dec a G * e_order A_dec b G.
-intros A op A_dec G comm a b Ha Hb Hab.
-assert (Hoat: 0 < e_order A_dec a G); try apply e_order_pos.
-assert (Hobt: 0 < e_order A_dec b G); try apply e_order_pos.
-assert (Hoabt: 0 < e_order A_dec (op a b) G); try apply e_order_pos.
-assert (Hoa: 0 <= e_order A_dec a G); auto with zarith.
-assert (Hob: 0 <= e_order A_dec b G); auto with zarith.
-apply Zle_antisym; apply Zdivide_le; auto with zarith.
-apply Zmult_lt_O_compat; auto.
-apply e_order_divide_gpow; sauto; auto with zarith.
-rewrite gpow_mult; auto with zarith.
-rewrite gpow_gpow; auto with zarith.
-rewrite gpow_e_order_is_e; auto with zarith.
-rewrite gpow_e; auto.
-rewrite Zmult_comm.
-rewrite gpow_gpow; auto with zarith.
-rewrite gpow_e_order_is_e; auto with zarith.
-rewrite gpow_e; auto.
-apply Zdivide_mult_rel_prime; auto.
-apply Gauss with (2 := Hab).
-apply e_order_divide_gpow; auto with zarith.
-rewrite <- (gpow_e _ _ G (e_order A_dec b G)); auto.
-rewrite <- (gpow_e_order_is_e _ A_dec  _ (op a b) G); auto with zarith.
-rewrite <- gpow_gpow; auto with zarith.
-rewrite (Zmult_comm (e_order A_dec (op a b) G)).
-rewrite gpow_mult; auto with zarith.
-rewrite gpow_gpow with (a := b); auto with zarith.
-rewrite gpow_e_order_is_e; auto with zarith.
-rewrite gpow_e; auto with zarith.
-rewrite G.(e_is_zero_r); auto with zarith.
-apply gpow_in; auto.
-apply Gauss with (2 := rel_prime_sym _ _ Hab).
-apply e_order_divide_gpow; auto with zarith.
-rewrite <- (gpow_e _ _ G (e_order A_dec a G)); auto.
-rewrite <- (gpow_e_order_is_e _ A_dec  _ (op a b) G); auto with zarith.
-rewrite <- gpow_gpow; auto with zarith.
-rewrite (Zmult_comm (e_order A_dec (op a b) G)).
-rewrite gpow_mult; auto with zarith.
-rewrite gpow_gpow with (a := a); auto with zarith.
-rewrite gpow_e_order_is_e; auto with zarith.
-rewrite gpow_e; auto with zarith.
-rewrite G.(e_is_zero_l); auto with zarith.
-apply gpow_in; auto.
-Qed.
-
-Theorem fermat_gen: forall (A : Set) (A_dec: forall (a b: A), {a = b} + {a <>b}) (op : A -> A -> A) (a: A) (G : FGroup op),
-       In a G.(s) ->  gpow a G (g_order G) = G.(e).
-intros A A_dec op a G H.
-assert (H1: (e_order A_dec a G | g_order G)).
-apply e_order_divide_g_order; auto.
-case H1; intros q; intros Hq; rewrite Hq.
-assert (Hq1: 0 <= q).
-apply Zmult_le_reg_r with (e_order A_dec a G); auto with zarith.
-apply Zlt_gt; apply e_order_pos.
-rewrite Zmult_0_l; rewrite <- Hq; apply Zlt_le_weak; apply g_order_pos.
-rewrite Zmult_comm; rewrite gpow_gpow; auto with zarith.
-rewrite gpow_e_order_is_e; auto with zarith.
-apply gpow_e; auto.
-apply Zlt_le_weak; apply e_order_pos.
-Qed.
-
-Theorem order_div: forall (A : Set) (A_dec: forall (a b: A), {a = b} + {a <>b}) (op : A -> A -> A) (a: A) (G : FGroup op) m,
- 0 < m -> (forall p, prime p -> (p | m) -> gpow a G (m / p) <> G.(e)) ->
- In a G.(s) -> gpow a G m = G.(e) -> e_order A_dec a G = m.
-intros A Adec op a G m Hm H H1 H2.
-assert (F1: 0 <= m); auto with zarith.
-case (e_order_divide_gpow A Adec op a G H1 m F1 H2); intros q Hq.
-assert (F2: 1 <= q).
-  case (Zle_or_lt 0 q); intros HH.
-    case (Zle_lt_or_eq _ _ HH); auto with zarith.
-    intros HH1; generalize Hm; rewrite Hq; rewrite <- HH1; 
-      auto with zarith.
-  assert (F2: 0 <= (- q) * e_order Adec a G); auto with zarith.
-    apply Zmult_le_0_compat; auto with zarith. 
-    apply Zlt_le_weak; apply e_order_pos.
-  generalize F2; rewrite Zopp_mult_distr_l_reverse;
-      rewrite <- Hq; auto with zarith.
-case (Zle_lt_or_eq _ _ F2); intros H3; subst; auto with zarith.
-case (prime_dec q); intros Hq.
-  case (H q); auto with zarith.
-    rewrite Zmult_comm; rewrite Z_div_mult; auto with zarith.
-  apply gpow_e_order_is_e; auto.
-case (Zdivide_div_prime_le_square _ H3 Hq); intros r (Hr1, (Hr2, Hr3)).
-case (H _ Hr1); auto.
-  apply Zdivide_trans with (1 := Hr2).
-  apply Zdivide_factor_r.
-case Hr2; intros q1 Hq1; subst.
-assert (F3: 0 < r).
-  generalize (prime_ge_2 _ Hr1); auto with zarith.
-rewrite <- Zmult_assoc; rewrite Zmult_comm; rewrite <- Zmult_assoc;
-  rewrite Zmult_comm; rewrite Z_div_mult; auto with zarith.
-rewrite gpow_gpow; auto with zarith.
-  rewrite gpow_e_order_is_e; try rewrite gpow_e; auto.
-  apply Zmult_le_reg_r with r; auto with zarith.
-  apply Zlt_le_weak; apply e_order_pos.
-apply Zmult_le_reg_r with r; auto with zarith.
-Qed.