proposition: Lemma ax6 : forall p q : positive, (Zpos p < Zpos q)%Z -> (Zpos p + Zneg q)%Z = Zneg (q - p).
proof: Proof. intros p q H'; red in H'. simpl in H'. simpl in |- *. rewrite Z.pos_sub_spec. rewrite H'. auto with *. Qed.
imports: Zring Group_kernel