proposition: Lemma Qquadratic_Qpositive_to_Qpositive_3_OO : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (hyp : quadraticAcc a b c d e f g h p1 p2), ~ quadratic_top_more a b c d e f g h -> ~ quadratic_top_more e f g h a b c d -> forall xs : Qpositive, p1 = dL xs -> forall ys : Qpositive, p2 = dL ys -> forall hyp_rec : quadraticAcc (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys, Qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 p2 hyp = Qquadratic_Qpositive_to_Qpositive (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys hyp_rec.
proof: Proof. intros. apply trans_eq with (Qquadratic_Qpositive_to_Qpositive a b c d e f g h (dL xs) (dL ys) (quadraticacc3_OO a b c d e f g h xs ys H H0 hyp_rec)). apply Qquadratic_Qpositive_to_Qpositive_equal_strong; reflexivity || assumption. unfold Qquadratic_Qpositive_to_Qpositive;fold Qquadratic_Qpositive_to_Qpositive; case (quadratic_top_more_informative a b c d e f g h); intros Habcdefgh; [ Falsum | idtac ]; case (quadratic_top_more_informative e f g h a b c d); intros Hefghabcd; [ Falsum | idtac ]; reflexivity. Qed.
imports: QArithSternBrocot(Merge_Order)