proposition: Lemma quadratic_top_more_3 : forall a b c d e f g h : Z, (0 < e + f + g + h)%Z -> (a - e + (b - f) + (c - g) + (d - h) < a + b + c + d)%Z.
proof: Proof. intros. apply Zplus_lt_reg_l with (e + f + g + h)%Z. apply Zplus_lt_reg_l with (- a - b - c - d)%Z. replace (- a - b - c - d + (e + f + g + h + (a - e + (b - f) + (c - g) + (d - h))))%Z with 0%Z. replace (- a - b - c - d + (e + f + g + h + (a + b + c + d)))%Z with (e + f + g + h)%Z. assumption. abstract ring. abstract ring. Qed.
imports: QArithSternBrocot(Merge_Order)