proposition: Lemma functor_star_leq {KA1: KleeneAlgebra G1} {KA2: KleeneAlgebra G2} {F: functor G1 G2} {HF: semiring_functor F}: forall A a, (F A A a)# <== F A A (a#).
proof: Proof. intros. apply star_destruct_left_one. rewrite <- functor_one. rewrite <- functor_dot. rewrite <- functor_plus. apply functor_incr. rewrite star_make_right. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(SemiLattice) ATBR(KleeneAlgebra)