fact: Fixpoint Mi i j:= if i is i.+1 then if j is j.+1 then Mi i j + (Mi i j.+1).*2 + Mi i j.+2 else Mi i 0 + Mi i 1 else (j==0):nat.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)