proposition: Lemma build_add: forall b i j s t M a, belong s M -> belong t M -> build b i j (add a s t M) [=0=] add a s t (build b i j M).
proof: Proof. induction b; intros i j s t M a Hs Ht ; cbn. apply add_comm. reflexivity. rewrite <- IHb1; auto. apply build_compat. rewrite <- IHb2; auto. apply build_compat. apply incr_add; trivial. rewrite <- IHb1; auto. apply build_compat. apply IHb2; trivial. unfold add_one. rewrite add_comm. apply add_compat. rewrite <- IHb; auto. apply build_compat. rewrite add_comm. apply add_compat. apply incr_add; trivial. apply add_comm. 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)