fact: Definition max_nonzero_subdef (xnz ynz : nullity) (xr yr : reality) := nz_of_bool (xnz && ynz || xnz && match xr with Real (Sign >=0) => true | _ => false end || ynz && xr && match yr with Real (Sign >=0) => true | _ => false end).
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)