proposition: Lemma Z_to_group_nat_neg : forall (p : positive) (r : G), Equal (Z_to_group_nat_fun r (Zneg p)) (Z_to_group_nat_fun (group_inverse G r) (Zpos p)).
proof: Proof. intros p r; 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 (nat_to_group (group_inverse G r) (nat_of_P (pos_abs (ax3 p)))); auto with algebra. Qed.
imports: Z_group