proposition: Lemma a_leq_star_a (a: X A A): a <== a#.
proof: Proof. rewrite <- star_make_left. rewrite <- one_leq_star_a. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)