proposition: Lemma pos_var_dist p q : 0 <= d(p , q).
proof: Proof. 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