proposition: Lemma uniq_decodable_f : uniquely_decodable f.
proof: Proof. elim => [ | a la H ]; case => [|b lb]; rewrite /extension /= /f //=; [by case : ifP |by case : ifP | ]. case: ifP => aT; case: ifP=> bT //; move /eqP; rewrite -/f eqseq_cat. + by case/andP=>[/eqP eq_ab ] /eqP /H ->; congr (_ :: _); apply: f_inj; rewrite /f aT bT. + by rewrite /= !/bitseq_of_nat !size_pad_seqL. + by case/andP=>[/eqP eq_ab ] /eqP /H ->; congr (_ :: _); apply: f_inj; rewrite /f aT bT. + by rewrite !size_tuple. 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