proposition: Lemma ax8 : forall p q : positive, Pcompare p q Datatypes.Eq = Datatypes.Lt -> Pcompare q p Datatypes.Eq = Datatypes.Gt.
proof: Proof. intros p q H'; try assumption. apply nat_of_P_gt_Gt_compare_complement_morphism. red in |- *. apply nat_of_P_lt_Lt_compare_morphism; auto with *. Qed.
imports: Zring Group_kernel