proposition: Lemma degree: degree_le (length (tl qpoints)) N.
proof: Proof. Proof with auto. intros. unfold N. apply degree_le_Sum. intros. apply in_map_iff in H. destruct H as [x [H H0]]. subst p. apply degree_le_mon with (length (tl x)). pose proof (ne_list.tails_are_shorter qpoints x H0). destruct x, qpoints; auto with arith. apply an_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