proposition: Lemma dominatesE A (Q P : A -> R) a : P `<< Q -> Q a = 0%R -> P a = 0%R.
proof: Proof. move/dominatesP; exact. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)