proposition: Lemma length_enum' n: length (enum' n) = n.
proof: Proof. Proof with auto with arith. induction n... simpl. rewrite map_length... 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