proposition: Lemma Σ_S_bound_front n f: Σ (S n) f == Σ n (f ∘ S) + f O.
proof: Proof. unfold Σ, Basics.compose. induction n; intros; simpl in *. ring. rewrite IHn. ring. 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