proposition: Lemma isweqletoleh (n m : nat) : isweq (letoleh n m).
proof: Proof. intros. set (is1 := isaprople n m). set (is2 := pr2 (n ≤ m)). apply (isweqimplimpl (letoleh n m) (natlehtole n m) is1 is2). Defined.
imports: UniMath.Foundations.NaturalNumbers