fact: Definition wider_nullity xnz ynz := match xnz, ynz with | MaybeZero, _ | NonZero, NonZero => true | NonZero, MaybeZero => false end.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)