proposition: Lemma natlthchoice2 (n m : nat) : n < m -> (S n < m) ⨿ ((S n) = m).
proof: Proof. intros l. induction (natlehchoice _ _ (natlthtolehsn _ _ l)) as [ l' | e ]. - apply (ii1 l'). - apply (ii2 e). Defined.
imports: UniMath.Foundations.Sets