proposition: Theorem ps_add_0_l : ∀ ps, (0 + ps = ps)%ps.
proof: Proof. intros ps. unfold ps_add; simpl. constructor. unfold ps_terms_add; simpl. rewrite Z.mul_1_r. unfold cm_factor. unfold cm; simpl. unfold ps_ordnum_add; simpl. rewrite Z.mul_1_r. unfold adjust_series. rewrite series_stretch_series_0. rewrite series_stretch_1. rewrite series_shift_series_0. rewrite series_add_0_l. rewrite <- Z2Nat_sub_min2. rewrite Z.min_id, Z.sub_0_r. rewrite Z.sub_diag, Nat.add_0_r. symmetry. remember (Z.to_nat (ps_ordnum ps)) as n eqn:Hn . rewrite ps_normal_adjust_eq with (n := n) (k := xH) in |- * at 1. subst n. unfold adjust_ps; simpl. rewrite Pos.mul_1_r, Z.mul_1_r. rewrite series_stretch_1. rewrite Z2Nat_id_max. rewrite <- Z.sub_min_distr_l. rewrite Z.sub_0_r, Z.sub_diag, Z.min_comm. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series