proposition: Theorem ps_monom_add_l : ∀ c d n, (ps_monom (c + d)%K n = ps_monom c n + ps_monom d n)%ps.
proof: Proof. intros c d n. unfold ps_monom; simpl. rewrite ps_adjust_eq with (n := 0%nat) (k := Qden n). unfold adjust_ps; simpl. rewrite series_shift_0. rewrite Z.sub_0_r. apply mkps_morphism; simpl. constructor; intros i; simpl. rewrite Z.min_id; simpl. rewrite Z.sub_diag; simpl. rewrite Nat.sub_0_r. destruct (zerop (i mod Pos.to_nat (Qden n))) as [H| H]. destruct (zerop (i / Pos.to_nat (Qden n))) as [H₁| H₁]. reflexivity. rewrite rng_add_0_l; reflexivity. rewrite rng_add_0_l; reflexivity. unfold ps_ordnum_add; simpl. rewrite Z.min_id; reflexivity. unfold cm; simpl. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat