proposition: Lemma Z_to_group_nat_fun_comp : forall (r r' : G) (n : Z), Equal r r' -> Equal (Z_to_group_nat_fun r n) (Z_to_group_nat_fun r' n).
proof: Proof. intros r r' n H'; try assumption. elim n. apply Trans with (monoid_unit G); auto with algebra. intros p; try assumption. apply Trans with (nat_to_group r (nat_of_P (pos_abs (ax3 p)))); auto with algebra. apply Trans with (nat_to_group r' (nat_of_P (pos_abs (ax3 p)))); auto with algebra. intros p; try assumption. apply Trans with (group_inverse G (nat_to_group r (nat_of_P (pos_abs (ax3 p))))); auto with algebra. apply Trans with (group_inverse G (nat_to_group r' (nat_of_P (pos_abs (ax3 p))))); auto with algebra. Qed.
imports: Z_group