proposition: Lemma wHb_1 : forall n l, size l = n -> HammingBitstring.wH l = 1%nat -> exists i, (i < n /\ l `b_ i = true)%nat /\ forall j, (j < n -> j <> i -> l `b_ j = false)%nat.
proof: Proof. elim. - by case. - move=> n IH [|[] t] // [Hsz] /=. + case=> H. exists O. split; first by []. move=> j Hj Hj'. destruct j => //=. move: (has_count (pred1 true) t). rewrite /HammingBitstring.wH /num_occ in H. rewrite H ltnn. move/negbT/hasPn => K. move: (@mem_nth _ false t j). rewrite ltnS in Hj. rewrite Hsz. move/(_ Hj). move/K => /= {}K. apply Bool.not_true_is_false. by apply/eqP. + rewrite add0n. case/(IH _ Hsz) => i [[H11 H12] H2]. exists i.+1%N. split; first by []. move=> j Hj Hj'. destruct j => //=. apply H2 => //. contradict Hj'; 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