fact: Definition fgle (D1 D2 : {freeg K / G}) := all [pred z | coeff z D1 <= coeff z D2] (dom D1 ++ dom D2).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)