proposition: Lemma Prod_StarE (s : seq letter) : (Prod s == Star) = [forall b, N(Bit (F2_of_bool b) | s) == N(Bit (F2_of_bool (~~ b)) | s)].
proof: Proof. apply/idP/idP => [| /forallP H0]. rewrite /Prod. case: ifP => //. move/negbT. rewrite -leqNgt leq_eqVlt. case/orP => [/eqP H1|H1]. rewrite H1 ltnn => _; apply/forallP; case; by apply/eqP. by rewrite H1. by rewrite /Prod (eqP (H0 true)) ltnn. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode