proposition: Theorem next_pow_add : ∀ p q L m, next_pow (p + q) L m = (next_pow p L m + q)%nat.
proof: Proof. intros p q L m. unfold next_pow. rewrite Nat.add_shuffle0; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM