proposition: Lemma top_more_informative : forall a b c d : Z, {top_more a b c d} + {~ top_more a b c d}.
proof: Proof. intros. case (quadro_leq_inf a b c d). intro. elim a0. intros. case (Z_le_lt_eq_dec c a H). intro. left. right. split. assumption. assumption. intro. case (Z_le_lt_eq_dec d b H0). intro. left. left. split. assumption. assumption. intro. right. intro. case H1. intro. elim H2. intros. rewrite e0 in H4. apply (Zgt_irrefl b). Flip. intro. elim H2. intros. rewrite e in H3. apply (Zgt_irrefl a). Flip. unfold top_more in |- *. intro. right. intro. case H. intro. apply n. elim H0. intros. split. assumption. apply Zlt_le_weak. assumption. intro. apply n. elim H0. intros. split. apply Zlt_le_weak. assumption. assumption. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)