proposition: Theorem nth_series_order_0_succ α (R : ring α) (K : field R) : ∀ s n i, nth_series_order K s i n = O → nth_series_order K s (S i) n = O.
proof: Proof. intros. revert i H. induction n; intros. simpl in H; simpl. remember (series_order s (S i)) as s1 eqn:Hs1; symmetry in Hs1. destruct s1 as [p1| ]; [ discriminate H | clear H ]. remember (series_order s (S (S i))) as s2 eqn:Hs2; symmetry in Hs2. destruct s2 as [p2| ]; [ exfalso | reflexivity ]. apply series_order_iff in Hs1; simpl in Hs1. apply series_order_iff in Hs2. destruct Hs2 as (_, Hs2). rewrite Nat.add_succ_l, <- Nat.add_succ_r in Hs2. apply Hs2, Hs1. simpl in H; simpl. remember (series_order s (S (S i))) as s2 eqn:Hs2; symmetry in Hs2. destruct s2 as [p2| ]; [ | reflexivity ]. remember (series_order s (S i)) as s1 eqn:Hs1; symmetry in Hs1. destruct s1 as [p1| ]. apply series_order_iff in Hs1; destruct Hs1 as (Hs11, Hs12). apply series_order_iff in Hs2; destruct Hs2 as (Hs21, Hs22). destruct p1. rewrite Nat.add_0_r in H, Hs12; clear Hs11. clear Hs21 Hs22. induction p2; [ rewrite Nat.add_0_r; apply IHn, H | ]. rewrite Nat.add_succ_r; apply IHn, IHp2. destruct (lt_eq_lt_dec p1 p2) as [[H1| H1]| H1]. apply Hs21 in H1. rewrite Nat.add_succ_l, <- Nat.add_succ_r in H1. exfalso; apply Hs12, H1. destruct H1. rewrite Nat.add_succ_r, <- Nat.add_succ_l in H. apply H. apply Nat.succ_lt_mono, Hs11 in H1. rewrite Nat.add_succ_r, <- Nat.add_succ_l in H1. exfalso; apply Hs22, H1. apply series_order_iff in Hs1; simpl in Hs1. apply series_order_iff in Hs2. destruct Hs2 as (_, Hs2). rewrite Nat.add_succ_l, <- Nat.add_succ_r in Hs2. exfalso; apply Hs2, Hs1. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series