proposition: Theorem nth_series_order_stretch : ∀ s b n k, nth_series_order K (series_stretch k s) (b * Pos.to_nat k) n = (Pos.to_nat k * nth_series_order K s b n)%nat.
proof: Proof. intros s b n k. revert b. induction n; intros. simpl. remember (series_order s (S b)) as len eqn:Hlen . symmetry in Hlen. destruct len as [len| ]. erewrite series_order_stretch_succ; eauto . rewrite Nat.mul_comm. remember (Pos.to_nat k * S len)%nat as x eqn:Hx . symmetry in Hx. destruct x; simpl. apply Nat.mul_eq_0 in Hx. destruct Hx as [Hx| Hx]; [ idtac | discriminate Hx ]. exfalso; revert Hx; apply Pos2Nat_ne_0. rewrite Nat.sub_0_r; reflexivity. rewrite series_order_stretch_succ_inf; [ idtac | assumption ]. rewrite Nat.mul_comm; reflexivity. simpl. remember (series_order s (S b)) as len eqn:Hlen . symmetry in Hlen. destruct len as [len| ]. erewrite series_order_stretch_succ; eauto . rewrite Nat.add_sub_assoc. rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_succ_r. remember (S (b + len) * Pos.to_nat k)%nat as x eqn:Hx . symmetry in Hx. destruct x; simpl. apply Nat.mul_eq_0 in Hx. destruct Hx as [Hx| Hx]; [ discriminate Hx | idtac ]. exfalso; revert Hx; apply Pos2Nat_ne_0. rewrite Nat.sub_0_r, <- Hx. apply IHn. remember (Pos.to_nat k) as kn eqn:Hkn . symmetry in Hkn. destruct kn; [ exfalso; revert Hkn; apply Pos2Nat_ne_0 | idtac ]. simpl; apply le_n_S, Nat.le_0_l. rewrite series_order_stretch_succ_inf; [ idtac | assumption ]. rewrite Nat.mul_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series