proposition: Theorem normalise_ps_1 : (normalise_ps 1 ≐ 1)%ps.
proof: Proof. remember (series_order (ps_terms 1%ps) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]. destruct n. constructor; simpl. erewrite ps_ordnum_normalise; try reflexivity; try eassumption. rewrite Z.add_0_r. remember Z.gcd as g; simpl; subst g. rewrite Z.gcd_0_l. rewrite Z.gcd_1_l. rewrite Z.div_0_l; [ reflexivity | idtac ]. intros H; discriminate H. erewrite ps_polydo_normalise; try reflexivity; try eassumption. remember Z.gcd as g; simpl; subst g. rewrite Z.gcd_1_l. reflexivity. erewrite ps_terms_normalise; try reflexivity; try eassumption. rewrite Z.add_0_r. remember Z.gcd as g; simpl; subst g. rewrite Z.gcd_0_l. rewrite Z.gcd_1_l. unfold normalise_series; simpl. rewrite series_shrink_1. rewrite series_left_shift_0; reflexivity. apply series_order_iff in Hn; simpl in Hn. destruct Hn as (_, Hn). exfalso; apply Hn; reflexivity. unfold normalise_ps. rewrite Hn. constructor; try reflexivity. constructor; intros i; simpl. apply series_order_iff in Hn. simpl in Hn. symmetry; apply Hn. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series