proposition: Lemma quadratic_top_more_1 : forall a b c d e f g h : Z, quadratic_top_more a b c d e f g h -> (0 < a - e + (b - f) + (c - g) + (d - h))%Z.
proof: Proof. intros. case H; [ intros (Hea, (Hfb, (Hgc, Hhd))) | intros [(Hea, (Hfb, (Hgc, Hhd)))| [(Hea, (Hfb, (Hgc, Hhd)))| (Hea, (Hfb, (Hgc, Hhd)))]] ]; replace 0%Z with (0 + 0 + 0 + 0)%Z; [ apply Zplus_le_lt_compat; [ repeat simple apply Zplus_le_0_compat | idtac ] | constructor | apply Zplus_lt_le_compat; [ apply Zplus_le_lt_compat; try apply Zplus_le_0_compat | idtac ] | constructor | apply Zplus_lt_le_compat; [ apply Zplus_lt_le_compat; [ apply Zplus_le_lt_compat | idtac ] | idtac ] | constructor | repeat apply Zplus_lt_le_compat | constructor ]; apply Zle_minus || apply Zaux.Zlt_minus; assumption. Qed.
imports: QArithSternBrocot(Merge_Order)