proposition: Lemma top_more_5' : forall a b c d : Z, (0 < a + b)%Z -> (a + b + (c - a) + (d - b) < a + b + c + d)%Z.
proof: Proof. intros. assert ((a + b + (c - a) + (d - b))%Z = (0 + (c + d))%Z). ring. rewrite H0. rewrite Zplus_assoc_reverse with (n := (a + b)%Z). apply Zplus_lt_le_compat. assumption. apply Z.le_refl. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)