proposition: 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.
proof: Proof. intros A op A_dec G comm a b Ha Hb Hab. assert (Hoat: 0 < e_order A_dec a G) by apply e_order_pos. assert (Hobt: 0 < e_order A_dec b G) by apply e_order_pos. assert (Hoabt: 0 < e_order A_dec (op a b) G) by apply e_order_pos. assert (Hoa: 0 <= e_order A_dec a G) by auto with zarith. assert (Hob: 0 <= e_order A_dec b G) by auto with zarith. apply Zle_antisym; apply Zdivide_le. 1, 4-5: 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.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange