proposition: Lemma aclosed : addr_closed C.
proof: Proof. split => [|? ? ? ?]; by [rewrite mem0v | rewrite rpredD]. 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