proposition: Lemma Mi_subsubdiag i : Mi i.+2 i = i.+2* i.*2.+1.
proof: Proof. elim: i => // i H; rewrite Mi_rec H Mi_subdiag Mi_diag !addn1 - addSn. rewrite mulSn -addSn -doubleS -{1}muln2 -mulnDr add2n -doubleS. by rewrite - (mul2n (i.+1).*2.+1) -mulnDl addn2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)