Fixpoint nat_dist_le m n : m ≤ n -> nat_dist m n = n-m. Proof. destruct m as [|m']. { destruct n as [|n']. { reflexivity. } { simpl. intros _. reflexivity. } } { destruct n as [|n']. { intro f. now induction (!natleh0tois0 f). } { exact (nat_dist_le m' n'). } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.