proposition: Lemma fm_uniq : uniquely_decodable fm.
proof: Proof. pose m' := m.-1. have mpos : m = m'.+1. rewrite prednK // -ltR_nat ltR_neqAle; split => //; exact/leR0n. have: (@extension [finType of 'rV[A]_n] _ f) \o (flatten \o map (fun x => @tval m _ (tuple_of_row x))) =1 @extension [finType of {: 'rV[ 'rV[A]_n ]_m} ] _ fm. by elim => //= ta sta; rewrite /extension /= map_cat flatten_cat => <-. apply: eq_inj. apply: inj_comp => //. rewrite mpos. elim => /= [| ta1 sta1 IHsta1]; case => [| ta2 sta2] //=. - move/(congr1 size); by rewrite size_cat size_map size_enum_ord addSn. - move/(congr1 size); by rewrite size_cat size_map size_enum_ord addSn. - move/eqP. rewrite eqseq_cat; last by rewrite !size_tuple. case/andP => H1 /eqP /IHsta1 ->. congr (_ :: _). exact/tuple_of_row_inj/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code