proposition: Lemma star_idem (a: X A A): a## == a#.
proof: Proof. apply leq_antisym. star_right_induction. rewrite star_trans. rewrite (one_leq_star_a a). auto with algebra. apply a_leq_star_a. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)