fact: Definition from {d T x0 nz cond} {x : @def d T x0 nz cond} (phx : phantom T x) := x.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)