proposition: Lemma incr_add : forall a s t M, belong s M -> belong t M -> incr (add a s t M) [=0=] add a s t (incr M).
proof: Proof. intros a s t [n M] Hs Ht. constructor. cbn in *. rewrite mx_point_blocks00 by assumption. rewrite mx_blocks_plus. auto with algebra. 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(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)