proposition: Lemma uniq_dec_inj (f : A -> seq B) : uniquely_decodable f -> injective f.
proof: Proof. rewrite /uniquely_decodable/extension. move=> f_uniq a1 a2 eq_f1_f2. move:(f_uniq [:: a1] [:: a2]); rewrite /= !cats0. by move=>tmp; move/tmp:eq_f1_f2=>[]. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext logb fdist proba