proposition: Lemma degree: degree_le (length (tl qpoints)) L.
proof: Proof. Proof with auto. unfold L. apply degree_le_Sum. intros ? H. destruct (proj1 (in_map_iff _ _ _) H) as [[[] v] [[] B]]. clear H. apply degree_le_mult_constant_l. clear crpoints. destruct qpoints. simpl in B. exfalso... simpl length. replace (@length (prod Q (RegularFunction Q_as_MetricSpace)) l) with (length (map (fun xi => (' (- fst xi)%Q[+X*][1])[*]_C_ (' (/ (q - fst xi)))) v) * 1)%nat. apply degree_le_Product. intros. destruct (proj1 (in_map_iff _ _ _) H) as [?[[]?]]. apply degree_le_mult_constant_r. apply degree_le_cpoly_linear_inv. apply (degree_le_c_ CRasCRing [1]). rewrite map_length. ring_simplify. apply eq_add_S. rewrite <- (separates_elem_lengths (p0 :: l) v)... replace v with (snd ((q, s), v))... apply in_map... 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