proposition: Lemma rank_cast_cols_comm : 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) (B : 'M[F]_(k, f k n)), \rank (cast_cols HPf HP B) = \rank B.
proof: Proof. move=> f P HPf k n HP. rewrite /cast_cols /eq_rect. 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