proposition: Lemma phi_f i : phi (f i) = i -> i \in S.
proof: Proof. rewrite /f; case: ifPn => // iS. rewrite /phi (_ : tuple_of_row _ = [tuple of nseq n false]); last first. rewrite -[RHS]row_of_tupleK; congr tuple_of_row. by apply/rowP => a; rewrite !mxE /tnth nth_nseq ltn_ord. rewrite /tuple2N /= /N_of_bitseq /= -{1}(cats0 (nseq n false)). rewrite rem_lea_false_nseq /= => defi. by rewrite -defi def_S in iS. 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