fact: Variables (R : Type) (idx : R) (op : Monoid.com_law idx) (I : choiceType) (J : choiceType) (K : choiceType).
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)