Definition nat_dist_between m n a b : nat_dist m n = a + b -> ∑ x:nat, nat_dist x m = a × nat_dist x n = b. Proof. intros j. induction (natgthorleh m n) as [r|s]. { apply nat_dist_between_ge. apply natlthtoleh. exact r. exact j. } { apply nat_dist_between_le. exact s. exact j. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.