proposition: Lemma quadratic_top_more_informative : forall a b c d e f g h : Z, {quadratic_top_more a b c d e f g h} + {~ quadratic_top_more a b c d e f g h}.
proof: Proof. intros. unfold quadratic_top_more in |- *. case (octet_leq_inf a b c d e f g h); [ idtac | right; red in |- *; intros [(H, (H1, (H2, H3)))| [(H, (H1, (H2, H3)))| [(H, (H1, (H2, H3)))| (H, (H1, (H2, H3)))]]]; apply n; repeat split; assumption || (apply Zlt_le_weak; assumption) ]. intros (H, (H1, (H2, H3))). case (Z_le_lt_eq_dec e a H); [ intro; left; repeat right; repeat split; assumption | intro; case (Z_le_lt_eq_dec f b H1); [ intro; left; do 2 right; left; repeat split; assumption | intro; case (Z_le_lt_eq_dec g c H2); [ intro; left; right; left; repeat split; assumption | intro; case (Z_le_lt_eq_dec h d H3); [ intro; repeat left; repeat split; assumption | intro; clear H H1 H2 H3; right; red in |- *; intros [(H, (H1, (H2, H3)))| [(H, (H1, (H2, H3)))| [(H, (H1, (H2, H3)))| (H, (H1, (H2, H3)))]]]; [ rewrite e3 in H3; apply Z.lt_irrefl with d; assumption | rewrite e2 in H2; apply Z.lt_irrefl with c; assumption | rewrite e1 in H1; apply Z.lt_irrefl with b; assumption | rewrite e0 in H; apply Z.lt_irrefl with a; assumption ] ] ] ] ]. Defined.
imports: QArithSternBrocot(Merge_Order)