proposition: Lemma Mi_subdiag i : Mi i.+1 i = i.*2+1.
proof: Proof. elim: i => // i H. by rewrite Mi_rec H Mi_diag Mi_zero // addn0 // addnAC -doubleD (addn1 i). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)