proposition: Theorem length_lap_mod_div_deg_1 : ∀ l c, length (lap_mod_div_deg_1 R l c) = length l.
proof: Proof. intros l c. induction l; [ reflexivity | simpl ]. rewrite IHl; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn