proposition: Lemma star_destruct_left_old' A B (a: X A A) (b c: X A B): b+a*c <== c -> a#*b <== c.
proof: Proof. intro H; transitivity (a#*c). rewrite <- H; semiring_reflexivity. apply star_destruct_left_c. rewrite <- H at -1; auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing)