proposition: Lemma nat_to_group_mult : forall (r : G) (n m : nat), Equal (nat_to_group r (n * m)) (nat_to_group (nat_to_group r n) m).
proof: Proof. simple induction m; simpl in |- *. rewrite mult_comm; simpl in |- *; auto with algebra. intros n0 H'; try assumption. rewrite mult_comm; simpl in |- *; auto with algebra. simpl in |- *. apply Trans with (sgroup_law G (nat_to_group r n) (nat_to_group r (n0 * n))); auto with algebra. apply Trans with (sgroup_law G (nat_to_group r (n0 * n)) (nat_to_group r n)); auto with algebra. apply SGROUP_comp; auto with algebra. rewrite mult_comm; simpl in |- *; auto with algebra. Qed.
imports: Z_group