proposition: Lemma Σ_constant x n f: (forall i, (i < n)%nat -> f i == x) -> Σ n f == inject_Z (Z.of_nat n) * x.
proof: Proof. Proof with auto. unfold Σ. induction n. reflexivity. simpl. intro E. rewrite IHn... rewrite E... rewrite P_of_succ_nat_Zplus. rewrite Q.Zplus_Qplus. 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