proposition: Lemma f_inj : injective f.
proof: Proof. have card_TS_Lt : (#|`TS P n epsilon| <= (expn 2 (Z.abs_nat L_typ)))%nat. by apply/leP; apply: INR_le; move: (card_le_TS_Lt n' P eps_pos); rewrite {1}cardsT card_tuple /= card_bool. move=> t1 t2; rewrite /f. case/boolP : (t1 == t2) ; first by move /eqP. move=> mainCase. case: ifP=>?; case: ifP=>? //; case=> H; last by apply/tuple_of_row_inj/inj_enc_not_typ/val_inj. - have {}H : index t1 (enum (`TS P n epsilon)) = index t2 (enum (`TS P n epsilon)) by apply (@bitseq_of_nat_inj (Z.abs_nat L_typ)) => //; apply: (leq_trans _ card_TS_Lt); apply: seq_index_enum_card => //; apply: enum_uniq. rewrite -(@nth_index _ t1 t1 (enum (`TS P n epsilon))); last by rewrite mem_enum. rewrite -(@nth_index _ t1 t2 (enum (`TS P n epsilon))); last by rewrite mem_enum. by rewrite H. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code