proposition: Lemma equiv_filter n p q (y m: X n n) (ia ib : X p n) (v : X n q): ia * y == ib * y -> y * m <== m * y -> y * v == v -> 1 <== y -> y * y <== y -> ia * m # * v == ib * m # * v.
proof: Proof. intros Hiy Hym Hyv H1y Hyy. rewrite <- Hyv, 2dot_assoc. monoid_rewrite (iter_equivalence H1y Hyy Hym). rewrite dot_assoc, Hiy. semiring_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)