fact: Definition Strassen := positive_rect (fun p => ('M_(p, p) -> 'M_(p, p) -> 'M_(p, p))) (@Strassen_xI) (@Strassen_xO) (fun M N => M *m N).
imports: ZArith Ncring Ncring_tac mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype) mathcomp(div finfun bigop prime binomial ssralg finset fingroup finalg) mathcomp(perm zmodp matrix) ssralg_ring_tac