proposition: Lemma quadratic_top_more_2 : forall a b c d e f g h : Z, quadratic_top_more a b c d e f g h -> (e + f + g + h < a + b + c + d)%Z.
proof: Proof. intros. case H; [ intros (Hea, (Hfb, (Hgc, Hhd))) | intros [(Hea, (Hfb, (Hgc, Hhd)))| [(Hea, (Hfb, (Hgc, Hhd)))| (Hea, (Hfb, (Hgc, Hhd)))]] ]; [ apply Zplus_le_lt_compat; [ repeat apply Zplus_le_compat | idtac ] | apply Zplus_lt_le_compat; [ apply Zplus_le_lt_compat; try apply Zplus_le_compat | idtac ] | apply Zplus_lt_le_compat; [ apply Zplus_lt_le_compat; [ apply Zplus_le_lt_compat | idtac ] | idtac ] | repeat apply Zplus_lt_le_compat ]; assumption. Qed.
imports: QArithSternBrocot(Merge_Order)