proposition: Lemma nat_to_group_mult : forall n m : nat, Equal (nat_to_group (ring_unit R) (n * m)) (ring_mult (nat_to_group (ring_unit R) n) (nat_to_group (ring_unit R) m)).
proof: Proof. simple induction n; simpl in |- *. auto with algebra. intros n0 H' m; try assumption. apply Trans with (sgroup_law R (nat_to_group (ring_unit R) m) (nat_to_group (ring_unit R) (n0 * m))); auto with algebra. apply Trans with (sgroup_law R (ring_mult (nat_to_group (ring_unit R) n0) (nat_to_group (ring_unit R) m)) (ring_mult (ring_unit R) (nat_to_group (ring_unit R) m))); auto with algebra. apply Trans with (sgroup_law R (ring_mult (nat_to_group (ring_unit R) n0) (nat_to_group (ring_unit R) m)) (nat_to_group (ring_unit R) m)); auto with algebra. apply Trans with (sgroup_law R (nat_to_group (ring_unit R) m) (ring_mult (nat_to_group (ring_unit R) n0) (nat_to_group (ring_unit R) m))); auto with algebra. Qed.
imports: Z_group_facts