proposition: Lemma vspace_not_empty (F : finFieldType) n (C : {vspace 'rV[F]_n}) : (0 < #| [set cw in C] |)%nat.
proof: Proof. apply/card_gt0P; exists 0; by rewrite inE mem0v. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup finalg perm) mathcomp(zmodp matrix vector order) mathcomp(lra mathcomp_extra Rstruct reals) Reals ssrR realType_ext Reals_ext ssr_ext ssralg_ext f2 fdist proba channel_code channel binary_symmetric_channel hamming pproba