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