proposition: Lemma Σ_wd f g n (H: forall x, (x < n)%nat -> f x == g x): Σ n f == Σ n g.
proof: Proof. Proof with auto with *. unfold Σ. induction n; simpl... rewrite IHn... rewrite H... 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