proposition: Lemma def_var_dist p q : d( p , q) = 0 -> p = q.
proof: Proof. rewrite /var_dist => H; apply/fdist_ext => a. rewrite -subR_eq0; apply/normR0_eq0; move: H. rewrite (bigD1 a) //= paddR_eq0 => [[] // | | ]; first exact/normR_ge0. by apply/RleP/sumr_ge0 => ? _; apply/RleP/normR_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrR Reals_ext Ranalysis_ext logb fdist ln_facts