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