proposition: Theorem ps_mul_inv_l : ∀ ps, (ps ≠ 0)%ps → (¹/ ps * ps = 1)%ps.
proof: Proof. intros ps Hps. remember (series_order (ps_terms ps) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]. assert (ps = ps_left_adjust ps)%ps as H by apply ps_left_adjust_eq. rewrite ps_mul_comm. rewrite H in |- * at 1. unfold ps_inv; simpl. unfold ps_left_adjust; simpl. rewrite Hn. unfold ps_mul; simpl. unfold cm_factor, cm; simpl. rewrite <- series_stretch_mul. rewrite series_mul_inv_r. rewrite stretch_series_1. rewrite <- Z.mul_add_distr_r. rewrite Z.add_sub_assoc, Z.add_opp_r. rewrite Z.add_comm, Z.add_simpl_r. rewrite Z.sub_diag, Z.mul_0_l. constructor. rewrite normalise_ps_1. unfold normalise_ps; simpl. remember (series_order 1%ser 0) as m eqn:Hm . symmetry in Hm. destruct m as [m| ]. destruct m; simpl. unfold gcd_ps. remember Z.gcd as g; simpl; subst g. rewrite Z.gcd_0_l. rewrite Z.div_0_l. rewrite greatest_series_x_power_series_1. rewrite Z.gcd_0_r; simpl. rewrite Z.div_same; [ idtac | apply Pos2Z_ne_0 ]. unfold normalise_series; simpl. rewrite series_left_shift_0. unfold series_shrink; simpl. constructor; try reflexivity; simpl. constructor; intros i; simpl. destruct i; [ reflexivity | idtac ]. remember (S i * Pos.to_nat (ps_polydo ps * ps_polydo ps))%nat as x. symmetry in Heqx; simpl. destruct x; [ idtac | reflexivity ]. apply Nat.eq_mul_0_l in Heqx; auto with Arith; discriminate Heqx. intros H₁. apply Z.gcd_eq_0_l in H₁. exfalso; revert H₁; apply Pos2Z_ne_0. apply series_order_iff in Hm; simpl in Hm. destruct Hm as (_, Hm). exfalso; apply Hm; reflexivity. apply series_order_iff in Hm; simpl in Hm. constructor; try reflexivity. constructor; intros i; simpl. symmetry; apply Hm. apply series_order_iff in Hn. destruct Hn as (Hz, Hnz). rewrite Nat.add_comm in Hnz; assumption. apply ps_series_order_inf_iff in Hn. contradiction. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series