Lemma nat_discern_isaprop m n : isaprop (nat_discern m n). Proof. revert n; induction m as [|m IHm]. { intros n. induction n as [|n IHn]. { apply isapropifcontr. apply iscontrunit. } { simpl. apply isapropempty. } } { intros n. induction n as [|n IHn]. { simpl. apply isapropempty. } { simpl. apply IHm. } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.