proposition: Theorem ps_monom_mul : ∀ a b m n, (ps_monom a m * ps_monom b n = ps_monom (a * b)%K (m + n))%ps.
proof: Proof. intros a b m n. progress unfold ps_mul; simpl. unfold cm; simpl. unfold ps_monom; simpl. apply mkps_morphism; try reflexivity. constructor; intros i; simpl. unfold convol_mul; simpl. destruct i; simpl. unfold summation; simpl. rewrite Nat.mod_0_l; [ idtac | apply Pos2Nat_ne_0 ]. rewrite Nat.mod_0_l; [ simpl | apply Pos2Nat_ne_0 ]. rewrite Nat.div_0_l; [ idtac | apply Pos2Nat_ne_0 ]. rewrite Nat.div_0_l; [ idtac | apply Pos2Nat_ne_0 ]. rewrite rng_add_0_r; reflexivity. rewrite all_0_summation_0; [ reflexivity | idtac ]. intros j (_, Hj). rewrite fold_sub_succ_l. destruct (zerop (j 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 (zerop c) as [H₁| H₁]. subst c. rewrite Nat.mul_0_l, Nat.sub_0_r. destruct (zerop (S i mod Pos.to_nat (Qden m))) as [H₁| H₁]. apply Nat.mod_divides in H₁; [ idtac | apply Pos2Nat_ne_0 ]. destruct H₁ as (d, Hd). rewrite Nat.mul_comm in Hd; rewrite Hd. rewrite Nat.div_mul; [ idtac | apply Pos2Nat_ne_0 ]. destruct (zerop d) as [H₁| H₁]; [ subst d; discriminate Hd | idtac ]. rewrite rng_mul_0_r; reflexivity. rewrite rng_mul_0_r; reflexivity. 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