proposition: Lemma Mi_zero i j : i < j -> Mi i j = 0.
proof: Proof. move: i j; elim => [[|j ] | i H [|j lij]] //. rewrite ltnS in lij; have lijw := (ltnW lij). rewrite /= !H // !ltnS //; exact: (leq_trans lijw (leqnSn j)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)