proposition: Lemma succ_not_in : ~ (fst (succ x y k) <= k <= snd (succ x y k)).
proof: Proof. unfold succ. destruct (total_order_T (middle x y) k) as [[Ho|Ho]|Ho]; simpl; intro Hn. destruct Hn as [_ Hn]; lra. assert (Hm: middle x (middle x y) < middle x y). apply Rlt_middle_r; apply Rlt_middle_l; assumption. destruct Hn as [_ [Hn|Hn]]; lra. destruct Hn as [Hn _]; lra. Qed.
imports: Reals Lra