proposition: Lemma nat_discern_isaprop m n : isaprop (nat_discern m n).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA