proposition: Theorem ps_add_opp_r : ∀ ps, (ps - ps = 0)%ps.
proof: Proof. intros ps. unfold ps_zero. unfold ps_add; simpl. constructor; simpl. unfold ps_opp; simpl. unfold ps_terms_add; simpl. unfold cm_factor; simpl. rewrite Z.min_id. rewrite Z.sub_diag; simpl. unfold adjust_series. do 2 rewrite series_shift_0. rewrite <- series_stretch_add_distr. rewrite series_add_opp_r. rewrite series_stretch_series_0. unfold ps_ordnum_add; simpl. unfold cm_factor, cm; simpl. rewrite Z.min_id. symmetry. remember (ps_polydo ps * ps_polydo ps)%positive as k eqn:Hk . rewrite ps_normal_adjust_eq with (n := O) (k := k); subst k. unfold adjust_ps; simpl. rewrite series_shift_0. rewrite series_stretch_series_0. remember (ps_ordnum ps) as v eqn:Hv . symmetry in Hv. destruct v as [| v| v]. reflexivity. symmetry. remember (Z.to_nat (ps_ordnum ps * Zpos (ps_polydo ps))) as n. rewrite ps_normal_adjust_eq with (n := n) (k := xH); subst n. unfold adjust_ps. remember Z.sub as g; simpl; subst g. rewrite series_stretch_series_0. rewrite series_shift_series_0. do 2 rewrite Pos.mul_1_r. rewrite Hv. rewrite Z2Nat.id; [ idtac | apply Pos2Z.is_nonneg ]. rewrite Z.sub_diag; reflexivity. remember (Z.to_nat (Zpos v * Zpos (ps_polydo ps))) as n. rewrite ps_normal_adjust_eq with (n := n) (k := xH); subst n. unfold adjust_ps. remember Z.sub as g; simpl; subst g. rewrite series_stretch_series_0. rewrite series_shift_series_0. rewrite positive_nat_Z; simpl. rewrite Pos.mul_1_r. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series