proposition: Lemma fgleP D1 D2 : reflect (forall z, coeff z D1 <= coeff z D2) (D1 <=g D2).
proof: Proof. apply: (iffP allP); last by move=> H z _; apply: H. move=> lec z; case z_in_dom: (z \in (dom D1 ++ dom D2)). exact: lec. move: z_in_dom; rewrite mem_cat; case/norP=> zD1 zD2. by rewrite !coeff_outdom // lexx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)