proposition: Lemma comm_iter_right: forall B A (x : X A B) a b, x * a == b * x -> x * a# == b# * x .
proof: Proof. exact (comm_iter_left (KA:=Dual.KleeneAlgebra)). Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)