proposition: Theorem eq_strong_ps_add_adjust_0_l : ∀ ps₁ ps₂ k, normalise_ps (ps₁ + ps₂)%ps ≐ normalise_ps (adjust_ps 0 k ps₁ + ps₂)%ps.
proof: Proof. intros ps₁ ps₂ k. rewrite ps_normal_adjust_eq with (n := O) (k := k). unfold ps_add; simpl. unfold adjust_ps; simpl. unfold ps_terms_add, ps_ordnum_add, adjust_series, cm, cm_factor; simpl. do 2 rewrite series_shift_0. do 2 rewrite Z.sub_0_r. rewrite series_stretch_add_distr. do 2 rewrite stretch_shift_series_distr. do 3 rewrite <- series_stretch_stretch. do 2 rewrite <- Z2Nat_inj_mul_pos_r. do 2 rewrite Z.mul_sub_distr_r. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. remember (ps_ordnum ps₁ * Zpos (ps_polydo ps₂) * Zpos k)%Z as x eqn:Hx . rewrite Z.mul_shuffle0 in Hx; rewrite <- Hx. rewrite Pos.mul_comm. remember (k * ps_polydo ps₁)%positive as y eqn:Hy . rewrite Pos.mul_comm in Hy; rewrite <- Hy. rewrite Pos_mul_shuffle0, <- Hy. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add