proposition: Theorem nth_series_order_0_add α (R : ring α) (K : field R) : ∀ s n i, nth_series_order K s i n = O → ∀ j, nth_series_order K s (i + j) n = O.
proof: Proof. intros. revert n i H. induction j; intros; [ rewrite Nat.add_0_r; apply H | ]. rewrite Nat.add_succ_r, <- Nat.add_succ_l. apply IHj, nth_series_order_0_succ, H. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series