Lemma natlehchoice4 (n m : nat) : n < S m -> (n < m) ⨿ (n = m). Proof. intros b. induction (natlthorgeh n m) as [p|p]. - exact (ii1 p). - exact (ii2 (isantisymmnatleh _ _ (natlthsntoleh _ _ b) p)). Defined.