Fixpoint nat_dist (m n:nat) : nat := match m , n with | S m, S n => nat_dist m n | 0, n => n | m, 0 => m end.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.