proposition: Lemma ax7 : forall p : positive, (Zpos p + Zneg p)%Z = 0%Z.
proof: Proof. intros p; try assumption. simpl in |- *. rewrite Z.pos_sub_spec; unfold Pos.compare. replace (Pcompare p p Datatypes.Eq) with Datatypes.Eq. auto with *. elim p. intros p0; simpl in |- *. auto with *. intros p0; simpl in |- *. auto with *. simpl in |- *. auto with *. Qed.
imports: Zring Group_kernel