fact: Definition dominates {R : realType} {A : Type} (Q P : A -> R) := locked (forall a, Q a = 0 -> P a = 0)%R.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)