proposition: Theorem ps_monom_add : ∀ a b n, (ps_monom a n + ps_monom b n = ps_monom (a + b)%K n)%ps.
proof: Proof. intros a b n. symmetry. unfold ps_add; simpl. unfold cm; simpl. unfold ps_ordnum_add; simpl. unfold ps_terms_add; simpl. rewrite ps_adjust_eq with (n := O) (k := Qden n). unfold adjust_ps; simpl. rewrite Z.sub_0_r. rewrite Z.min_id. apply mkps_morphism; try reflexivity. rewrite series_shift_0. rewrite Z.sub_diag; simpl. unfold adjust_series; simpl. do 2 rewrite series_shift_0. constructor; intros i; simpl. destruct (zerop (i mod Pos.to_nat (Qden n))) as [H₁| H₁]. apply Nat.mod_divides in H₁; [ idtac | apply Pos2Nat_ne_0 ]. destruct H₁ as (c, Hc). rewrite Nat.mul_comm in Hc; rewrite Hc. rewrite Nat.div_mul; [ idtac | apply Pos2Nat_ne_0 ]. destruct c; [ reflexivity | simpl ]. rewrite rng_add_0_l; reflexivity. rewrite rng_add_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series