proposition: Theorem ps_mul_1_l : ∀ ps, (1 * ps = ps)%ps.
proof: Proof. intros ps. constructor. unfold normalise_ps; simpl. unfold cm, cm_factor; simpl. rewrite stretch_series_1, series_mul_1_l. rewrite series_stretch_1. remember (series_order (ps_terms ps) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]; [ idtac | reflexivity ]. constructor; simpl. rewrite Z.mul_1_r; f_equal. rewrite stretch_series_1, series_stretch_1, series_mul_1_l. unfold gcd_ps; simpl. rewrite Z.mul_1_r; reflexivity. do 2 f_equal. rewrite stretch_series_1, series_stretch_1, series_mul_1_l. unfold gcd_ps; simpl. rewrite Z.mul_1_r; reflexivity. do 2 rewrite stretch_series_1 in |- * at 1. do 2 rewrite series_stretch_1 in |- * at 1. rewrite series_mul_1_l. unfold gcd_ps; simpl. rewrite Z.mul_1_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat