proposition: Lemma sum_collapse': forall k f b (j: state), (j<k)%nat -> sum 0 k (fun i => xif (eqb (state_of_nat i) j && b i) (f i) (0: regex)) == xif (b j) (f j) 0.
proof: Proof. intros. rewrite (sum_collapse (n:=j)); auto. cbn. rewrite id_num. bool_simpl. reflexivity. intros. num_analyse. num_lia. 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)