proposition: Lemma algebraic_correctness: forall A B C (j' j n m': X B B) (u u': X A B) (v v': X B C), j'==j# -> m'==n*j' -> u'==u*j' -> v'==v -> u*(j+n)#*v == u'*m'#*v'.
proof: Proof. intros. rewrite H0, H1, H2, H. rewrite star_distr. 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(DKA_Definitions) ATBR(Utils_WF) Coq(Relations) Coq(Eqdep_dec)