proposition: Lemma StrassenP p : mulmx =2 (Strassen (p := p)).
proof: Proof. elim: p => // [p IHp|p IHp] M N. rewrite /= /Strassen_xI; case:ifP=> // _. by rewrite Strassen_stepP // -mulmx_block !submxK -mulmx_cast castmxK. rewrite /= /Strassen_xO; case:ifP=> // _. by rewrite Strassen_stepP // -mulmx_cast castmxK. Qed.
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