proposition: Lemma succ_compat : fst (succ x y k) < snd (succ x y k).
proof: Proof. unfold succ. destruct (total_order_T (middle x y) k) as [[_|_]|_]; simpl; repeat (apply Rlt_middle_r || apply Rlt_middle_l); assumption. Qed.
imports: Reals Lra