proposition: Lemma a_star_a_leq_star_a: forall (a: X A A), a*a# <== a#.
proof: Proof. exact (star_a_a_leq_star_a (KA:=Dual.KleeneAlgebra) (A:=A)). Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)