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