proposition: Lemma move_star2 A B (a: X A B) (b: X B A): (a*b)#*a == a*(b*a)#.
proof: Proof. apply comm_iter_left. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)