proposition: Lemma additive_sbound_f' k (H : k.-1 <= n) : additive (sbound_f' H).
proof: Proof. by move=> x y; rewrite sbound_f'D sbound_f'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