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