Definition nat_dist_between_ge m n a b : n ≤ m -> nat_dist m n = a + b -> ∑ x:nat, nat_dist x m = a × nat_dist x n = b. Proof. intros i j. rewrite nat_dist_symm in j. rewrite natpluscomm in j. exists (pr1 (nat_dist_between_le n m b a i j)). apply (weqdirprodcomm _ _). exact (pr2 (nat_dist_between_le n m b a i j)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.