proposition: Theorem ps_monom_mul_r_pow : ∀ c p n, (ps_monom c (Qnat n * p) = ps_monom c 0 * ps_monom 1%K p ^ n)%ps.
proof: Proof. intros c p n. induction n; simpl. rewrite rng_mul_1_r. progress unfold Qnat; simpl. rewrite Qmult_0_l; reflexivity. rewrite ps_mul_assoc. rewrite rng_mul_shuffle0; simpl. rewrite <- IHn. assert (Qnat (S n) * p == Qnat n * p + p) as H. progress unfold Qnat; simpl. rewrite Zpos_P_of_succ_nat. progress unfold Qmult, Qplus; simpl. progress unfold Qeq. simpl. rewrite <- Z.mul_add_distr_r. rewrite Pos2Z.inj_mul. symmetry. rewrite <- Z.mul_assoc. apply Z.mul_cancel_r. simpl. apply Pos2Z_ne_0. progress unfold Z.succ; simpl. rewrite Z.mul_add_distr_r. rewrite Z.mul_1_l; reflexivity. rewrite H. rewrite ps_monom_add_r. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol