proposition: Lemma functor_incr: forall A B, Proper ((leq A B) ==> (leq _ _)) (F A B).
proof: Proof. intros. intros x y H. unfold leq. rewrite <- functor_plus. apply functor_compat. trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(SemiLattice) ATBR(KleeneAlgebra)