proposition: Lemma lang_sum: forall (f: nat -> language) w n i, sum i n f w <-> exists2 j, j<n & f (i+j)%nat w.
proof: Proof. induction n. - compute. firstorder. lia. - intros j. simpl. unfold lang_union. rewrite IHn. clear IHn. intuition. exists O; auto with arith. rewrite Nat.add_comm. assumption. destruct H0 as [k ? ?]. exists (Datatypes.S k); auto with arith. rewrite <- plus_n_Sm. assumption. destruct H as [[|k] ? ?]. + left. rewrite Nat.add_comm in H0. assumption. + right. exists k; auto with arith. rewrite <- plus_n_Sm in H0. assumption. Qed.
imports: Coq(List) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(Functors) ATBR(MxFunctors) ATBR(DKA_Definitions) ATBR(Model_Languages)