Fixpoint nat_dist_symm m n : nat_dist m n = nat_dist n m. Proof. destruct m as [|m']. { destruct n as [|n']. { reflexivity. } { simpl. reflexivity. } } { destruct n as [|n']. { simpl. reflexivity. } { simpl. apply nat_dist_symm. } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.