proposition: Lemma iter_equivalence n (y m: X n n): 1 <== y -> y * y <== y -> y * m <== m * y -> m# * y == y * (m * y)#.
proof: Proof. intros H1y Hyy Hym. apply comm_iter_left. apply leq_antisym. rewrite <- H1y at 2. semiring_reflexivity. rewrite dot_assoc, Hym. monoid_rewrite Hyy. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties)