proposition: Lemma f_phi i : i \in S -> phi (f i) = i.
proof: Proof. move=> iS; rewrite /f iS /phi row_of_tupleK. have H : ((index i (enum S)).+1 < expn 2 n)%nat. have : ((index i (enum S)).+1 <= #| S |)%nat. by apply seq_index_enum_card => //; exact: enum_uniq. by move/leq_ltn_trans; exact. move Heq1 : (tuple2N _) => eq1. case: eq1 Heq1 => [|i0 Heq1]. - case/tuple2N_0 => Heq1. have : (seq.index i (enum S)).+1 <> O by []. by move=> /bitseq_of_nat_nseq_false/(_ H); rewrite Heq1. - move Heq : ((Npos i0).-1 < #| S |)%nat => []. - by rewrite -Heq1 /= N_of_bitseq_bitseq_of_nat // nth_index // mem_enum. - move: Heq. by rewrite -Heq1 /tuple2N N_of_bitseq_bitseq_of_nat// seq_index_enum_card // enum_uniq. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext ssralg_ext logb natbin fdist proba entropy aep typ_seq source_code