proposition: Theorem order_pow : ∀ a n, (a ≠ 0)%ps → (order (a ^ n) = qfin (Qnat n) * order a)%Qbar.
proof: Proof. intros a n Ha. induction n; simpl. remember (order a) as v eqn:Hv . symmetry in Hv. destruct v as [v| ]. unfold Qnat; simpl. rewrite Qmult_0_l. unfold ps_one. rewrite ps_monom_order; [ reflexivity | idtac ]. intros H; apply Ha. rewrite <- ps_mul_1_l. unfold ps_one. rewrite H, ps_zero_monom_eq. rewrite ps_mul_0_l. reflexivity. exfalso; apply Ha. apply order_inf; assumption. rewrite order_mul. rewrite IHn. remember (order a) as v eqn:Hv . symmetry in Hv. destruct v as [v| ]; [ simpl | reflexivity ]. rewrite <- Nat.add_1_l. unfold Qnat. rewrite Nat2Z.inj_add, QZ_plus. rewrite Qmult_plus_distr_l; simpl. rewrite Qmult_1_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m