proposition: Lemma minSS i j : minn i.+1 j.+1 = (minn i j).+1.
proof: Proof. by rewrite !minnE subSS subSn // leq_subr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)