proposition: Lemma Strassen_stepP (p : positive) (A B : 'M[R]_(p + p)) f : f =2 mulmx -> Strassen_step A B f = A *m B.
proof: Proof. move=> Hf; rewrite -{2}[A]submxK -{2}[B]submxK mulmx_block /Strassen_step !Hf. rewrite /GRing.add /= /GRing.opp /=. by congr block_mx; non_commutative_ring. 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