proposition: Lemma Prod_cons (x : letter) h t : Prod [:: h] = x /\ (Prod t = x \/ Prod t = Star) -> Prod (h :: t) = x.
proof: Proof. case=> H1 H2. rewrite /Prod /=. case/letterP : h H1 => /=; rewrite {1}/Prod /= => ?; subst x; rewrite ?(addn0,addn1,add0n). - case: H2; rewrite {1}/Prod. case: ifPn => [H3 _|]. by rewrite ltnS leq_eqVlt H3 orbT. rewrite -leqNgt leq_eqVlt. case/orP => [/eqP ->|->//]. by rewrite ltnn. case: ifPn => //; rewrite -leqNgt leq_eqVlt. case/orP => [/eqP|] -> //. rewrite ltnn => _ /=; by rewrite ltnS leqnn. - case: H2; rewrite {1}/Prod. case: ifPn => [//|]. rewrite -leqNgt leq_eqVlt. case/orP => [/eqP ->|H3]. by rewrite ltnn. rewrite H3 => _. rewrite {1}add1n (leq_trans _ (leqnSn _)) // ltnNge ltnW //. by apply/leq_trans: H3. case: ifPn => //. rewrite -leqNgt leq_eqVlt. case/orP => [/eqP|] -> //. rewrite ltnn => _. by rewrite add1n ltnSn /= ltnNge leqnSn. - by case: H2. - by case: H2. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode