proposition: Lemma split_lt_succ : forall n m : nat, lt n (S m) -> lt n m \/ n = m.
proof: Proof. intros n m. generalize dependent n. induction m. - intros. destruct n. + right. reflexivity. + exfalso. inversion H. inversion H1. - intros. destruct n. + left. unfold lt. apply -> Nat.succ_le_mono; apply Nat.le_0_l. + apply Nat.lt_succ_lt_pred in H. simpl in H. specialize (IHm n H). destruct IHm. * left. apply -> Nat.succ_lt_mono. assumption. * subst. right. reflexivity. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon