proposition: Lemma star_destruct_left_one A: forall (a c: X A A), 1+a*c <== c -> a# <== c.
proof: Proof. intros. rewrite <- (dot_neutral_right (a#)). apply star_destruct_left_old. assumption. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)