proposition: Lemma interpolates_economically: @interpolates_economically CRasCField crpoints (N qpoints).
proof: Proof. split. apply interpolates. unfold crpoints. rewrite ne_list.list_map, tl_map, map_length. apply degree. Qed.
imports: CoRN.model.totalorder.QposMinMax Unicode.Utf8 Setoid Arith List Program Permutation metric2.Classified CSetoids CPoly_ApZero CPoly_Degree CRArith CRArith_alg Qmetric Qring CReals Ranges stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation CRings