proposition: Lemma quadraticacc_3_OI : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), quadraticAcc a b c d e f g h p1 p2 -> forall xs ys : Qpositive, p1 = dL xs -> p2 = nR ys -> ~ quadratic_top_more a b c d e f g h -> ~ quadratic_top_more e f g h a b c d -> quadraticAcc (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys.
proof: Proof. simple destruct 1; intros; try solve [ Falsum ]; match goal with | id1:(dL _ = nR _) |- _ => discriminate id1 | id1:(nR _ = dL _) |- _ => discriminate id1 | id1:_ |- _ => idtac end; (rewrite H0 in H2; discriminate H2) || (rewrite H1 in H4; discriminate H4) || (try let T_local1 := eval compute in (f_equal Qpositive_tail H3) in let T_local2 := eval compute in (f_equal Qpositive_tail H4) in (rewrite <- T_local1; rewrite <- T_local2; assumption)). Defined.
imports: QArithSternBrocot(Merge_Order)