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