proposition: Theorem poly_compose_compose2 : ∀ α (r : ring α) P Q, (P ∘ Q = poly_compose2 P Q)%pol.
proof: Proof. intros α r P Q. apply lap_compose_compose2. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn