fact: Definition cmΣ' {M: CMonoid} (n: nat) (f: sig (ge n) → M): M := cm_Sum (map f (enum' n)).
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