proposition: Lemma wHb_2 : forall n l, size l = n -> HammingBitstring.wH l = 2%nat -> (exists i, exists k, (i < n /\ l `b_ i = true) /\ (k < n /\ l `b_ k = true) /\ i <> k /\ forall j, j < n -> j <> i -> j <> k -> l `b_ j = false)%nat.
proof: Proof. elim. - by case. - case. move=> IH l Hsz Hcount. rewrite /HammingBitstring.wH /num_occ in Hcount. move: (count_size (pred1 true) l). by rewrite Hcount Hsz ltnn. - move=> n IH [|[] t] // [Hsz] /=. + rewrite add1n. case=> X. exists O. case: (@wHb_1 _ _ Hsz X) => k [[Hk1 Hk11] Hk2]. exists k.+1%N. split; first by []. split; first by split => //; exact: (@leq_ltn_trans n.+1%N). split; first by []. move=> j Hj Hj' Hjk. destruct j => //=. apply Hk2 => //. contradict Hjk; by rewrite Hjk. + rewrite add0n. case/(IH _ Hsz) => i [k [[H11 H12] [H21 [H221 H222]]]]. exists i.+1%N, k.+1%N. split; first by []. split; first by []. split. contradict H221; by case: H221. move=> j Hj Hj' Hjk. destruct j => //=. apply H222 => //. contradict Hj'; by subst j. contradict Hjk; by subst j. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext