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