proposition: Lemma symmetric_var_dist p q : d(p , q) = d(q , p).
proof: Proof. rewrite /var_dist; apply eq_bigr => ? _; by rewrite distRC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrR Reals_ext Ranalysis_ext logb fdist ln_facts