Definition nat_dist_between_le m n a b : m ≤ n -> nat_dist m n = a + b -> ∑ x, nat_dist x m = a × nat_dist x n = b. Proof. intros i j. exists (m+a). split. { apply nat_dist_plus. } { rewrite (nat_dist_le m n i) in j. assert (k := natminuseqlr _ _ _ i j); clear j. assert (l := nat_dist_plus (m+a) b). rewrite nat_dist_symm. rewrite (natpluscomm (a+b) m) in k. rewrite (natplusassoc m a b) in l. rewrite <- k in l. exact l. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.