proposition: Lemma quadraticacc_0' : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), quadraticAcc a b c d e f g h p1 p2 -> p1 <> One -> p2 = One -> homographicAcc (a + b) (c + d) (e + f) (g + h) p1.
proof: Proof. intros; inversion H; trivial; try solve [ Falsum ]; rewrite H1 in H14; discriminate H14. Defined.
imports: QArithSternBrocot(Merge_Order)