fact: Fixpoint degree_plus_1_of_list α {R : ring α} (zerop : ∀ a, {(a = 0)%K} + {(a ≠ 0)%K}) (l : list α) := match l with | [] => O | [x … l₁] => match degree_plus_1_of_list zerop l₁ with | O => if zerop x then O else 1%nat | S n => S (S n) end end.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn