proposition: Lemma pi_mon : forall f, Vmonotone (pi f) Dge (@Lgt f%).
proof: Proof. unfold Vmonotone, Vmonotone_i, RelUtil.monotone. intros. rewrite Lge_is_eq, H0. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)