proposition: Theorem ps_ordnum_normalise : ∀ ps n p vn, series_order (ps_terms ps) 0 = fin n → p = greatest_series_x_power K (ps_terms ps) n → vn = (ps_ordnum ps + Z.of_nat n)%Z → ps_ordnum (normalise_ps ps) = (vn / Z.gcd vn (Z.gcd (Zpos (ps_polydo ps)) (Z.of_nat p)))%Z.
proof: Proof. intros ps n p vn Hn Hp Hvn. unfold normalise_ps; simpl. rewrite Hn; simpl. rewrite <- Hp. unfold gcd_ps; simpl. rewrite <- Z.gcd_assoc. rewrite <- Hvn. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat