proposition: Theorem e_order_divide_gpow: forall n, 0 <= n -> gpow n = G.(e) -> (e_order | n).
proof: Proof. 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 (Z.abs_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 (Z.abs_nat n - 1)). apply support_aux_in; auto with zarith. rewrite <- (fun x => Zabs_nat_Z_of_nat (@length A x)). replace (Z.abs_nat n - 1)%nat with (Z.abs_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. rewrite Z.abs_eq by auto with zarith. rewrite inj_minus1. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. apply inj_le_rev; rewrite inj_Zabs_nat; simpl. rewrite Z.abs_eq; auto with zarith. rewrite inj_minus1. rewrite inj_Zabs_nat. rewrite Z.abs_eq. rewrite Zplus_comm; simpl; auto with zarith. auto with zarith. apply inj_le_rev; rewrite inj_Zabs_nat; simpl. rewrite Z.abs_eq; auto with zarith. exists 0; auto with arith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange