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