proposition: Lemma interpolates_economically (qpoints: ne_list (Q * CR)): QNoDup (map fst qpoints) → interpolates_economically (ne_list.map (first inject_Q_CR) qpoints) (L qpoints).
proof: Proof. Proof with auto. split. rewrite ne_list.list_map. apply interpolates... rewrite ne_list.list_map. rewrite tl_map. rewrite map_length. apply degree... Qed.
imports: Unicode.Utf8 Setoid Arith List Program Permutation CSetoids CRings CPoly_Degree CPoly_ApZero CRArith Qmetric Qring CReals stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation