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 -> homographicAcc (a + c) (b + d) (e + g) (f + h) p2.
proof: Proof. intros; inversion H; trivial; try solve [ Falsum ]; rewrite H0 in H12; discriminate H12. Defined.
imports: QArithSternBrocot(Merge_Order)