proposition: Theorem ps_mul_add_distr_l : ∀ ps₁ ps₂ ps₃, (ps₁ * (ps₂ + ps₃) = ps₁ * ps₂ + ps₁ * ps₃)%ps.
proof: Proof. intros ips₁ ips₂ ips₃. rewrite <- (normalise_ps_eq ips₁). rewrite <- (normalise_ps_eq ips₂). rewrite <- (normalise_ps_eq ips₃). remember (normalise_ps ips₁) as ps₁ eqn:Hps₁ . remember (normalise_ps ips₂) as ps₂ eqn:Hps₂ . remember (normalise_ps ips₃) as ps₃ eqn:Hps₃ . remember (ps_ordnum ps₁ * Zpos (ps_polydo ps₂) * Zpos (ps_polydo ps₃))%Z as vcc. remember (Zpos (ps_polydo ps₁) * ps_ordnum ps₂ * Zpos (ps_polydo ps₃))%Z as cvc. remember (Zpos (ps_polydo ps₁) * Zpos (ps_polydo ps₂) * ps_ordnum ps₃)%Z as ccv. remember ((vcc + Z.min cvc ccv) * Zpos (ps_polydo ps₁))%Z as n₁. remember ((vcc + Z.min cvc ccv) * Zpos (ps_polydo ps₁))%Z as n₂. do 2 rewrite eq_ps_add_add₂. rewrite ps_adjust_eq with (n := O) (k := ps_polydo ps₁); symmetry. rewrite ps_adjust_eq with (n := O) (k := xH); symmetry. remember (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃))%ps as ps₄ eqn:Hps₄ . remember (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂) (ps₁ * ps₃)))%ps as ps₅ eqn:Hps₅ . remember (series_order (ps_terms ps₄) 0) as n₄ eqn:Hn₄ . remember (series_order (ps_terms ps₅) 0) as n₅ eqn:Hn₅ . symmetry in Hn₄, Hn₅. assert (n₄ = n₅) as H by (subst; apply null_range_length_mul_add₂_distr_l). move H at top; subst n₅. destruct n₄ as [n₄| ]. constructor; constructor; simpl. eapply ps_ordnum_adjust_normalise_mul_add₂_distr_l; eassumption. eapply ps_polydo_adjust_normalise_mul_add₂_distr_l; eassumption. eapply ps_terms_adjust_normalise_mul_add₂_distr_l; eassumption. rewrite ps_series_order_inf_iff in Hn₄. rewrite ps_series_order_inf_iff in Hn₅. rewrite Hn₄, Hn₅; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat