proposition: Lemma ae_eq_mul1l f g : ae_eq f (cst 1) -> ae_eq g (g \* f).
proof: Proof. by apply: filterS => x /[apply] ->; rewrite mule1. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)