proposition: Lemma semicomm_iter_right B (a: X A A) (b: X B B) (c: X B A): c*a <== b*c -> c*a# <== b#*c.
proof: Proof. intro H. star_right_induction. monoid_rewrite H. rewrite <- star_make_left at 2. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)