proposition: 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).
proof: Proof. 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 Z.lt_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.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange