fact: Definition applybig {R I} (body : bigbody R I) x := let: BigBody _ op b v := body in if b then op v x else x.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)