proposition: Theorem ps_left_adjust_eq : ∀ ps, (ps = ps_left_adjust ps)%ps.
proof: Proof. intros ps. remember (series_order (ps_terms ps) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]. constructor; constructor; simpl. erewrite ps_ordnum_normalise; try reflexivity; try eassumption. erewrite ps_ordnum_normalise with (n := O); try reflexivity; try eassumption. rewrite Z.add_0_r. unfold ps_left_adjust. rewrite Hn. remember Z.gcd as g; simpl; subst g. rewrite greatest_series_x_power_left_shift. rewrite Nat.add_0_r; reflexivity. eapply series_order_left_adjust; eassumption. erewrite ps_polydo_normalise; try reflexivity; try eassumption. erewrite ps_polydo_normalise with (n := O); try reflexivity; try eassumption. rewrite Z.add_0_r. unfold ps_left_adjust. rewrite Hn. remember Z.gcd as g; simpl; subst g. rewrite greatest_series_x_power_left_shift. rewrite Nat.add_0_r; reflexivity. eapply series_order_left_adjust; eassumption. erewrite ps_terms_normalise; try reflexivity; try eassumption. erewrite ps_terms_normalise with (n := O); try reflexivity; try eassumption. rewrite Z.add_0_r. unfold ps_left_adjust. rewrite Hn. remember Z.gcd as g; simpl; subst g. rewrite greatest_series_x_power_left_shift. rewrite Nat.add_0_r. unfold normalise_series. rewrite series_left_shift_0; reflexivity. eapply series_order_left_adjust; eassumption. constructor; constructor; simpl. unfold normalise_ps. rewrite Hn. rewrite series_order_inf_left_adjust; [ reflexivity | idtac ]. assumption. unfold normalise_ps. rewrite Hn. rewrite series_order_inf_left_adjust; [ reflexivity | idtac ]. assumption. unfold normalise_ps. rewrite Hn. rewrite series_order_inf_left_adjust; [ reflexivity | idtac ]. assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series