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