proposition: Theorem ps_monom_add_r : ∀ c p q, (ps_monom c (p + q) = ps_monom c p * ps_monom 1%K q)%ps.
proof: Proof. intros c p q. unfold ps_mul; simpl. unfold cm; simpl. unfold ps_monom; simpl. apply mkps_morphism; try reflexivity. unfold ps_mul; simpl. unfold cm; simpl. unfold ps_monom; simpl. constructor; intros i; simpl. unfold series_stretch; simpl. unfold convol_mul; simpl. destruct i; simpl. rewrite summation_only_one; simpl. rewrite Nat.mod_0_l; auto with Arith; simpl. rewrite Nat.mod_0_l; auto with Arith; simpl. rewrite Nat.div_0_l; auto with Arith; simpl. rewrite Nat.div_0_l; auto with Arith; simpl. rewrite rng_mul_1_r; reflexivity. rewrite all_0_summation_0; [ reflexivity | simpl ]. intros j (_, Hj). destruct j; simpl. rewrite Nat.mod_0_l; auto with Arith; simpl. rewrite Nat.div_0_l; auto with Arith; simpl. destruct (zerop (S i mod Pos.to_nat (Qden p))) as [H| H]. apply Nat.mod_divides in H; auto with Arith. destruct H as (d, Hd). rewrite Nat.mul_comm in Hd; rewrite Hd. rewrite Nat.div_mul; auto with Arith. destruct d; [ discriminate Hd | simpl ]. rewrite rng_mul_0_r; reflexivity. rewrite rng_mul_0_r; reflexivity. destruct (zerop (S j mod Pos.to_nat (Qden q))) as [H| H]. apply Nat.mod_divides in H; auto with Arith. destruct H as (d, Hd). rewrite Nat.mul_comm in Hd; rewrite Hd. rewrite Nat.div_mul; auto with Arith. destruct d; [ discriminate Hd | simpl ]. rewrite rng_mul_0_l; reflexivity. rewrite rng_mul_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat