proposition: Lemma quadraticacc_1 : 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 -> quadratic_top_more a b c d e f g h -> quadraticAcc (a - e) (b - f) (c - g) (d - h) e f g h p1 p2.
proof: Proof. simple destruct 1; intros; trivial; try solve [ Falsum ]. Defined.
imports: QArithSternBrocot(Merge_Order)