proposition: Theorem divide_g_order_e_order: forall n, 0 <= n -> (n | g_order IA) -> exists a, In a IA.(s) /\ e_order A_dec a IA = n.
proof: Proof. intros n Hn H. assert (Hg: 0 < g_order IA). apply g_order_pos. assert (He: forall a, 0 <= e_order A_dec a IA). intros a; apply Zlt_le_weak; apply e_order_pos. pattern n; apply prime_div_induction with (n := g_order IA); auto. exists e; split; auto. apply IA.(e_in_s). apply Zle_antisym. apply Zdivide_le; auto with zarith. apply e_order_divide_gpow; auto with zarith. apply IA.(e_in_s). rewrite gpow_1; auto. apply IA.(e_in_s). match goal with |- (_ <= ?X) => assert (0 < X) end; try apply e_order_pos; auto with zarith. intros p i Hp Hi K. assert (Hp1: 0 < p). apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. assert (Hi1: 0 < p ^ i). apply Zpower_gt_0; auto. case Zle_lt_or_eq with (1 := Hi); clear Hi; intros Hi; subst. case (not_all_solutions (g_order IA / p)). apply Zdivide_Zdiv_lt_pos; auto with zarith. apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. apply Z.divide_trans with (2 := K). apply Zpower_divide; auto. intros a (Ha1, Ha2). exists (gpow a IA (g_order IA / p ^ i)); split. apply gpow_in; auto. match goal with |- ?X = ?Y => assert (H1: (X | Y) ) end; auto. apply e_order_divide_gpow; auto with zarith. apply gpow_in; auto. rewrite <- gpow_gpow; auto with zarith. rewrite Zmult_comm; rewrite <- Zdivide_Zdiv_eq; auto with zarith. apply fermat_gen; auto. apply Z_div_pos; auto with zarith. case prime_power_div with (4 := H1); auto with zarith. intros j ((Hj1, Hj2), Hj3). case Zle_lt_or_eq with (1 := Hj2); intros Hj4; subst; auto. case Ha2. replace (g_order IA) with (((g_order IA / p ^i) * p ^ j) * p ^ (i - j - 1) * p). rewrite Z_div_mult; auto with zarith. repeat rewrite gpow_gpow; auto with zarith. rewrite <- Hj3. rewrite gpow_e_order_is_e; auto with zarith. rewrite gpow_e; auto. apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. apply gpow_in; auto. apply Z_div_pos; auto with zarith. apply Zmult_le_0_compat; try apply Z_div_pos; auto with zarith. pattern p at 4; rewrite <- Zpower_1_r. repeat rewrite <- Zmult_assoc; repeat rewrite <- Zpower_exp; auto with zarith. replace (j + (i - j - 1 + 1)) with i; auto with zarith. apply sym_equal; rewrite Zmult_comm; apply Zdivide_Zdiv_eq; auto with zarith. rewrite Zpower_0_r; exists e; split. apply IA.(e_in_s). match goal with |- ?X = 1 => assert (tmp: 0 < X); try apply e_order_pos; case Zle_lt_or_eq with 1 X; auto with zarith; clear tmp; intros H1 end. absurd (gpow IA.(FGroup.e) IA 1 = IA.(FGroup.e)). apply gpow_e_order_lt_is_not_e with A_dec; auto with zarith. apply gpow_e; auto with zarith. intros p q H1 (a, (Ha1, Ha2)) (b, (Hb1, Hb2)). exists (mult a b); split. apply IA.(internal); auto. rewrite <- Ha2; rewrite <- Hb2; apply order_mult; auto. rewrite Ha2; rewrite Hb2; auto. Qed.
imports: ZCAux List Root UList IGroup EGroup FGroup