Fixpoint nat_dist_gt m n : m > n -> S (nat_dist m (S n)) = nat_dist m n. Proof. destruct m as [|m']. { unfold natgth; simpl. intro x. apply fromempty. apply nopathsfalsetotrue. exact x. } { intro i. simpl. destruct n as [|n']. { apply (maponpaths S). apply nat_dist_m0. } { simpl. apply nat_dist_gt. exact i. } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.