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