proposition: Lemma phi_f x : phi (f x) = x.
proof: Proof. rewrite /phi. case:(pickP _)=> [x0 /eqP | H]. - by apply: f_inj. - by move: (H x); rewrite eqxx. 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