fact: Definition wider_sign xs ys := match xs, ys with | NonNeg, NonNeg | NonNeg, EqZero | NonPos, NonPos | NonPos, EqZero | EqZero, EqZero => true | NonNeg, NonPos | NonPos, NonNeg | EqZero, NonPos | EqZero, NonNeg => false end.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)