proposition: Lemma leq_var_dist (p q : {fdist A}) x : `| p x - q x | <= d( p , q ).
proof: Proof. rewrite /var_dist (bigD1 x) //= -{1}(addR0 `| p x - q x |). by apply/leR_add2l/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