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