proposition: Lemma star_trans (a: X A A): a#*a# == a#.
proof: Proof. apply leq_antisym. star_right_induction. rewrite star_a_a_leq_star_a. reflexivity. rewrite <- one_leq_star_a at 3. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)