proposition: Lemma nat_to_group_com3 : forall n : nat, Equal (sgroup_law G (nat_to_group n) (group_inverse G r)) (sgroup_law G (group_inverse G r) (nat_to_group n)).
proof: Proof. simple induction n; simpl in |- *; auto with *. apply Trans with (group_inverse G r); auto with *. intros n0 H'; try assumption. apply Trans with (sgroup_law G (nat_to_group n0) (sgroup_law G r (group_inverse G r))); auto with *. apply Trans with (sgroup_law G (nat_to_group n0) (monoid_unit G)); auto with *. apply Trans with (nat_to_group n0); auto with *. apply Trans with (sgroup_law G (group_inverse G r) (sgroup_law G r (nat_to_group n0))); auto with *. apply Trans with (sgroup_law G (sgroup_law G (group_inverse G r) r) (nat_to_group n0)); auto with *. apply Trans with (sgroup_law G (monoid_unit G) (nat_to_group n0)); auto with *. Qed.
imports: Zring Group_kernel