proposition: Lemma wH_1 n (x : 'rV['F_2]_n) : wH x = 1%nat -> exists i : 'I_n, x ``_ i = 1%R /\ (forall j : 'I_n, i <> j -> x ``_ j = 0%R).
proof: Proof. rewrite wH_bitstring. move/wHb_1. move/(_ n). rewrite size_tuple. case/(_ erefl) => i [] [] H1 H2 H3. exists (Ordinal H1); split. transitivity (F2_of_bool true) => //. rewrite -H2 /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple. rewrite (_ : _ _ _ i = (tuple_of_row x) !_ (Ordinal H1)); last first. apply set_nth_default; by rewrite size_tuple. rewrite tnth_mktuple {1}(F2_0_1 (x ``_ (Ordinal H1))); by case: (x ``_ _ != 0%R). move=> j Hj. transitivity (F2_of_bool false) => //. rewrite -(H3 j) //; last first. move=> ?; subst i. by apply/Hj/val_inj. rewrite /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple. suff -> : x ``_ j = nth ord0 (tuple_of_row x) j by apply: F2_0_1. rewrite (_ : _ _ _ j = (tuple_of_row x) !_ j); last by rewrite tnth_mktuple. exact: tnth_nth. 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