proposition: Theorem series_stretch_iff_const : ∀ k s c, (series_stretch k s = series_const c)%ser ↔ (s = series_const c)%ser.
proof: Proof. intros k s c. split; intros H. constructor; intros i. inversion_clear H as (s₁, s₂, Hi). simpl in Hi; simpl. pose proof Hi (i * Pos.to_nat k)%nat as H. rewrite Nat.mod_mul in H; [ simpl in H | apply Pos2Nat_ne_0 ]. rewrite Nat.div_mul in H; [ simpl in H | apply Pos2Nat_ne_0 ]. destruct (zerop i) as [H₁| H₁]; [ subst i; assumption | ]. destruct (zerop (i * Pos.to_nat k)) as [H₂| ]; [ | assumption ]. apply Nat.mul_eq_0_l in H₂; [ | apply Pos2Nat_ne_0 ]. exfalso; subst i; revert H₁; apply Nat.lt_irrefl. rewrite H. apply series_stretch_const. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series