proposition: Lemma mulmx_perm : forall n (s t : 'S_n), perm_mx s *m perm_mx t === perm_mx (s * t).
proof: Proof. move=> n s t i j; rewrite/mulmx/perm_mx. setoid_rewrite (bigD1 (j:=s i))=>//=. setoid_rewrite (big1 (P:=fun k => k != s i))=>[|k]; first by rewrite eq_refl permM; ring. by rewrite eq_sym; move/negbTE => ->; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms