proposition: Theorem series_order_succ2 : ∀ s m, series_order s (S m) = series_order (series_left_shift m s) 1.
proof: Proof. intros s m. remember (series_order s (S m)) as n eqn:Hn . symmetry in Hn |- *. apply series_order_iff in Hn. apply series_order_iff. destruct n as [n| ]. destruct Hn as (Hz, Hnz). split. intros i Hin; simpl. rewrite Nat.add_succ_r, <- Nat.add_succ_l. apply Hz; assumption. simpl. rewrite Nat.add_succ_r, <- Nat.add_succ_l. assumption. simpl; intros i. rewrite Nat.add_succ_r, <- Nat.add_succ_l. apply Hn. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series