proposition: Lemma pi_monotone_eq : monotone I Dge.
proof: Proof. intro f. unfold Dge. apply Vmonotone_transp. apply (coef_pos_monotone_peval_Dle (PI_WM f)). Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)