fact: Fixpoint lap_mod_div_deg_1 α (r : ring α) la c := match la with | [] => [] | [a₁ … la₁] => [apply_lap la c … lap_mod_div_deg_1 r la₁ c] end.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn