proposition: Lemma Σ_plus_bound m n f: Σ (m + n) f == Σ n f + Σ m (f ∘ plus n).
proof: Proof. Proof with try reflexivity. induction m; simpl; intros. unfold Σ. simpl. ring. do 2 rewrite Σ_S_bound_back. rewrite Qplus_assoc. rewrite <- IHm. unfold Basics.compose. replace (f (m + n)%nat) with (f (n + m)%nat)... rewrite Nat.add_comm... Qed.
imports: CoRN.stdlib_omissions.List Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric Coq.Program.Program CoRN.stdlib_omissions.N CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q