Fixpoint helper_A m n : nat_dist m n = 0 -> nat_discern m n. Proof. destruct m as [|m']. { destruct n as [|n']. { intros _. exact tt. } { simpl. exact (negpathssx0 n'). } } { destruct n as [|n']. { simpl. exact (negpathssx0 m'). } { simpl. exact (helper_A m' n'). } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.