proposition: Lemma leq_addE m1 m2 n1 n2 : m1 <= m2 -> n1 <= n2 -> m1 + n1 = m2 + n2 -> m1 = m2 /\ n1 = n2.
proof: Proof. move=> lem len eqD; have [_] := leqif_add (leqif_eq lem) (leqif_eq len). by rewrite eqD eqxx => /esym/andP[/eqP->/eqP->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)