fact: Definition dominatesb {A : finType} (Q P : A -> R) := [forall b, (Q b == 0%R) ==> (P b == 0%R)].
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)