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