proposition: Lemma cmΣ'_constant (c: CR) (n: nat): cmΣ' n (λ _, c) == ' n * c.
proof: Proof. Proof with auto. unfold cmΣ'. rewrite (cm_Sum_constant c). rewrite map_length, length_enum'. reflexivity. intros. apply in_map_iff in H. destruct H. symmetry. destruct H. subst. reflexivity. Qed.
imports: Unicode.Utf8 Program CRArith CRabs Qminmax Qauto Qround Qmetric stdlib_omissions.P stdlib_omissions.Z stdlib_omissions.Q stdlib_omissions.N metric2.Classified util.Container Ranges decision