proposition: Lemma comm_iter_left A B (x : X A B) a b: a * x == x * b -> a# * x == x * b# .
proof: Proof. intro H. apply leq_antisym. apply semicomm_iter_left, equal_leq. trivial. apply semicomm_iter_right, equal_leq. auto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)