proposition: Lemma castmx_cols_mulmx2 : forall (f : nat -> nat -> nat) P (HPf : forall k n, P k n -> f k n = n) k n (HP : P k n) (X : 'M[R]_(f k n, f k n)) cols (Y : 'M_(f k n, cols)), castmx (HPf _ _ HP, HPf _ _ HP) X *m castmx (HPf _ _ HP, erefl cols) Y = castmx (HPf _ _ HP, erefl cols) (X *m Y).
proof: Proof. move=> f P HPf k n_ HP X cols Y; apply/matrixP => i j. rewrite !mxE /=. move: (HPf _ _ HP) X Y; rewrite (HPf _ _ HP) => e M Y. rewrite castmxE !mxE /=. apply eq_bigr => l _ /=. rewrite !castmxE /=. congr (M _ _ * Y _ _); by apply val_inj. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code