proposition: Lemma quadratic_top_more_4_2 : forall a b c d e f g h : Z, quadratic_top_more a b c d e f g h -> (f <= b)%Z.
proof: Proof. intros. case H; [ intros (Hea, (Hfb, (Hgc, Hhd))) | intros [(Hea, (Hfb, (Hgc, Hhd)))| [(Hea, (Hfb, (Hgc, Hhd)))| (Hea, (Hfb, (Hgc, Hhd)))]] ]; assumption || (apply Zlt_le_weak; assumption). Qed.
imports: QArithSternBrocot(Merge_Order)