proposition: Lemma succ_included_r : snd (succ x y k) <= y.
proof: Proof. unfold succ. destruct (total_order_T (middle x y) k) as [[_|_]|_]; simpl. left; apply Rlt_middle_r; assumption. left; apply Rlt_trans with (r2 := (middle x y)); repeat (apply Rlt_middle_r || apply Rlt_middle_l); assumption. right; reflexivity. Qed.
imports: Reals Lra