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