proposition: Lemma top_more_3 : forall a b c d : Z, (0 < c + d)%Z -> (a - c + (b - d) < a + b)%Z.
proof: Proof. intros. apply Zplus_lt_reg_l with (c + d)%Z. apply Zplus_lt_reg_l with (- a - b)%Z. replace (- a - b + (c + d + (a - c + (b - d))))%Z with 0%Z. replace (- a - b + (c + d + (a + b)))%Z with (c + d)%Z. assumption. ring. ring. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)