proposition: Theorem eq_strong_ps_add_add₂ : ∀ ps₁ ps₂, (ps₁ + ps₂)%ps ≐ ps_add₂ ps₁ ps₂.
proof: Proof. intros ps₁ ps₂. constructor; [ simpl | reflexivity | simpl ]. unfold ps_ordnum_add. rewrite Z2Nat.id. rewrite Z.sub_sub_distr. rewrite Z.sub_diag; simpl. apply Z.min_comm. rewrite <- Z.sub_max_distr_l. rewrite Z.sub_diag. apply Z.le_max_r. unfold ps_terms_add. unfold adjust_series. unfold cm_factor. remember (ps_ordnum ps₂ * Zpos (ps_polydo ps₁))%Z as vc₂₁. remember (ps_ordnum ps₁ * Zpos (ps_polydo ps₂))%Z as vc₁₂. remember (Z.min vc₁₂ vc₂₁) as m eqn:Hm . rewrite Z.min_comm, <- Hm. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series