proposition: Lemma sbound_f'Z k (H : k.-1 <= n) a y : sbound_f' H (a *: y) = a *: sbound_f' H y.
proof: Proof. by apply/rowP => i; rewrite !mxE. 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