proposition: Theorem lap_mod_deg_1_apply : ∀ la c, (lap_mod_deg_1 la c = 0)%K → (apply_lap la c = 0)%K.
proof: Proof. intros la c Hmod. destruct la as [| a]; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn