proposition: Lemma mulmx_castmx_cols_comm2 : forall (f : nat -> nat -> nat) (P : nat -> nat -> Type) (HPf: forall k n, P k n -> f k n = n) k n (HP : P k n) rows (x : 'M[R]_(f k n, rows)) cols (B : 'M_(rows, cols)), castmx (HPf _ _ HP, erefl rows) x *m B = castmx (HPf _ _ HP, erefl cols) (x *m B).
proof: Proof. move=> f P HPf k n_ HP. move: (HPf k n_ HP); rewrite (HPf k n_ HP) => e. by rewrite (eq_irrelevance e (refl_equal n_)). 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