proposition: Lemma Qquadratic_signok_0 : forall (e f g h : Z) (p2 : Qpositive), Qquadratic_sg_denom_nonzero e f g h One p2 -> Qhomographic_sg_denom_nonzero (e + g) (f + h) p2.
proof: Proof. intros. inversion H. inversion H1. apply Qhomographic_signok0. assumption. replace (e + g + (f + h))%Z with (e + f + (g + h))%Z. assumption. abstract ring. assumption. Defined.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)