proposition: Lemma le1 (d : t) a : d a <= 1.
proof: Proof. rewrite -(f1 d) (_ : d a = \sum_(a' in A | a' == a) d a'). rewrite big_mkcond /=. apply: ler_sum => a0 _. case: ifPn => // _. exact: ge0. by rewrite big_pred1_eq. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext