proposition: Lemma Qquadratic_signok_4 : forall (e f g h : Z) (p1 p2 : Qpositive), Qquadratic_sg_denom_nonzero e f g h (dL p1) (dL p2) -> Qquadratic_sg_denom_nonzero (e + f + g + h) (f + h) (g + h) h p1 p2.
proof: Proof. intros. inversion H. discriminate H0. discriminate H0. assumption. Defined.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)