proposition: Lemma a_star_a_leq_star_a_a (a: X A A): a*a# <== a#*a.
proof: Proof. star_right_induction. rewrite star_a_a_leq_star_a at 1. apply plus_destruct_leq; auto. rewrite <- one_leq_star_a. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)