proposition: Theorem eq_strong_ps_adjust_zero_neg_zero : ∀ ps, series_order (ps_terms ps) 0 = ∞ → ∃ n₁ n₂ k₁ k₂, eq_ps_strong (adjust_ps n₁ k₁ ps) (adjust_ps n₂ k₂ ps_neg_zero).
proof: Proof. intros ps Hz. unfold normalise_ps in Hz. remember (series_order (ps_terms ps) 0) as n eqn:Hn . symmetry in Hn. destruct n; [ discriminate Hz | clear Hz ]. apply series_order_iff in Hn. simpl in Hn. destruct (Z_le_dec 0 (ps_ordnum ps)) as [H₁| H₁]. exists (Z.to_nat (ps_ordnum ps + Zpos (ps_polydo ps))), O, xH, (ps_polydo ps). constructor; simpl. rewrite Z2Nat.id. rewrite Z.mul_1_r. rewrite Z.sub_add_distr, Z.sub_diag; reflexivity. apply Z.add_nonneg_nonneg; [ assumption | idtac ]. apply Pos2Z.is_nonneg. rewrite Pos.mul_1_r; reflexivity. rewrite series_stretch_series_0. rewrite series_shift_series_0. rewrite series_stretch_1. constructor; intros i. rewrite series_nth_0_series_nth_shift_0. rewrite series_nth_series_0; reflexivity. assumption. exists (Pos.to_nat (ps_polydo ps)). exists (Z.to_nat (- ps_ordnum ps)). exists xH, (ps_polydo ps). constructor; simpl. rewrite Z.mul_1_r. rewrite Z2Nat.id; [ idtac | fast_omega H₁ ]. rewrite Z.opp_involutive. remember (ps_ordnum ps) as v. rewrite positive_nat_Z. destruct v; [ reflexivity | reflexivity | simpl ]. rewrite Pos.add_comm; reflexivity. rewrite Pos.mul_1_r; reflexivity. rewrite series_stretch_1. rewrite series_stretch_series_0. constructor; intros i. rewrite series_nth_0_series_nth_shift_0. rewrite series_shift_series_0. rewrite series_nth_series_0; reflexivity. assumption. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add