proposition: Theorem series_order_shift_S : ∀ s c n, (c ≤ n)%nat → series_order (series_shift (S n) s) c = NS (series_order (series_shift n s) c).
proof: Proof. intros s c n Hcn. remember (series_order (series_shift n s) c) as u eqn:Hu . remember (series_order (series_shift (S n) s) c) as v eqn:Hv . symmetry in Hu, Hv. apply series_order_iff in Hu. apply series_order_iff in Hv. destruct u as [u| ]. destruct Hu as (Hiu, Hu). destruct v as [v| ]. destruct Hv as (Hiv, Hv). apply Nbar.fin_inj_wd. rewrite series_nth_shift_S in Hu. destruct (lt_dec (S u) v) as [Hlt₁| Hge₁]. rewrite <- Nat.add_succ_r in Hu. rewrite Hiv in Hu; [ negation Hu | assumption ]. apply Nat.nlt_ge in Hge₁. destruct v. simpl in Hv. exfalso. rewrite Nat.add_0_r in Hv. destruct (lt_dec c (S n)) as [H₂| H₂]. apply Hv; reflexivity. apply H₂. apply Nat.succ_le_mono in Hcn; assumption. destruct (lt_dec v u) as [Hlt₂| Hge₂]. apply Hiu in Hlt₂. rewrite Nat.add_succ_r in Hv. rewrite <- series_nth_shift_S in Hv; contradiction. apply Nat.nlt_ge in Hge₂. apply le_antisym; [ assumption | idtac ]. apply Nat.succ_le_mono in Hge₂; assumption. rewrite series_nth_shift_S in Hu. rewrite <- Nat.add_succ_r in Hu. exfalso; apply Hu, Hv. destruct v as [v| ]; [ idtac | reflexivity ]. destruct Hv as (Hiv, Hv). destruct v. rewrite Nat.add_0_r in Hv. exfalso. simpl in Hv. destruct (lt_dec c (S n)) as [H₂| H₂]. apply Hv; reflexivity. apply H₂. apply Nat.succ_le_mono in Hcn; assumption. rewrite Nat.add_succ_r in Hv. rewrite <- series_nth_shift_S in Hv. exfalso; apply Hv, Hu. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series