proposition: Lemma top_more_2 : forall a b c d : Z, top_more a b c d -> (c + d < a + b)%Z.
proof: Proof. intros. case H. intros. elim H0. intros. apply Zplus_le_lt_compat. assumption. assumption. intros. elim H0. intros. apply Zplus_lt_le_compat. assumption. assumption. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)