Definition natleorle m n : (m≤n) ⨿ (n≤m). Proof. intros. induction (natgthorleh m n) as [r|s]. { apply ii2. apply natlthtoleh. exact r. } { apply ii1. exact s. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.