proposition: Lemma Zl3 : forall p : positive, Equal (Z_to_group_nat_fun (Zneg p)) (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 p))))).
proof: Proof. intros p; try assumption. unfold Z_to_group_nat_fun in |- *. case (Z_gt_le_dec (Zneg p) 0); intros z. absurd (Zneg p > 0)%Z; auto with *. case (Z_le_lt_eq_dec (Zneg p) 0 z); intros. simpl in |- *; auto with *. inversion e. Qed.
imports: Zring Group_kernel