proposition: Lemma Z_to_group_nat_inv : forall (n : Z) (r : G), Equal (Z_to_group_nat_fun r (- n)%Z) (Z_to_group_nat_fun (group_inverse G r) n).
proof: Proof. simple induction n; simpl in |- *. intros r; try assumption. apply Trans with (monoid_unit G); auto with algebra. auto with algebra. intros p r; try assumption. apply Trans with (Z_to_group_nat_fun (group_inverse G (group_inverse G r)) (Zpos p)); auto with algebra. Qed.
imports: Z_group