proposition: Theorem normalise_ps_add_adjust : ∀ ps₁ ps₂ n k m, normalise_ps (adjust_ps m k ps₁ + ps₂)%ps ≐ normalise_ps (adjust_ps n k ps₁ + ps₂)%ps.
proof: Proof. intros ps₁ ps₂ n k m. do 2 rewrite eq_strong_ps_normal_add_add₂. unfold ps_add₂; simpl. unfold adjust_ps_from. unfold cm_factor; simpl. do 2 rewrite ps_adjust_adjust. rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. remember (ps_ordnum ps₁) as v₁. remember (ps_polydo ps₂) as c₂. remember (ps_ordnum ps₂) as v₂. remember (ps_polydo ps₁) as c₁. remember (Z.of_nat n) as nn. remember (Z.of_nat m) as mm. do 2 rewrite Z.mul_sub_distr_r. replace n with (Z.to_nat nn) by (rewrite Heqnn, Nat2Z.id; reflexivity). replace m with (Z.to_nat mm) by (rewrite Heqmm, Nat2Z.id; reflexivity). do 2 rewrite <- Z2Nat_inj_mul_pos_r. rewrite <- Z2Nat.inj_add. rewrite <- Z2Nat.inj_add. do 2 rewrite <- Z.sub_add_distr. do 2 rewrite <- Z.add_sub_swap. do 2 rewrite Z.sub_add_distr. do 2 rewrite Z.add_simpl_r. rewrite Z.mul_shuffle0. remember (v₁ * Zpos c₂ * Zpos k)%Z as vc₁. remember (v₂ * Zpos c₁ * Zpos k)%Z as vc₂. rewrite <- Z2Nat_sub_min2. rewrite <- Z2Nat_sub_min1. rewrite Z.min_id, Z.sub_diag, Nat.add_0_r. rewrite <- Z2Nat_sub_min2. rewrite <- Z2Nat_sub_min1. rewrite Z.min_id, Z.sub_diag, Nat.add_0_r. do 4 rewrite Z.sub_sub_distr. rewrite Z.add_comm. rewrite Z.add_sub_assoc. rewrite Z.add_sub_swap. rewrite <- Z.sub_sub_distr. symmetry. rewrite Z.add_comm. rewrite Z.add_sub_assoc. rewrite Z.add_sub_swap. rewrite <- Z.sub_sub_distr. symmetry. rewrite Z2Nat.inj_sub. symmetry. rewrite Z2Nat.inj_sub. rewrite Z.add_comm. destruct (Z_le_dec vc₁ vc₂) as [H₁| H₁]. rewrite Z2Nat.inj_add. rewrite Z.add_comm. rewrite Z2Nat.inj_add. rewrite Z.min_l; auto. rewrite Z.sub_diag. do 2 rewrite Nat.sub_0_r. rewrite <- Z2Nat_sub_min. rewrite Z.min_l; auto. rewrite Z.sub_diag, Nat.add_0_r. rewrite Nat.add_0_r. replace (Z.to_nat (nn * Zpos c₂)) with (Z.to_nat (nn * Zpos c₂) + 0)%nat by fast_omega. rewrite <- Nat.add_assoc; simpl. rewrite normalise_ps_adjust_add. replace (Z.to_nat (mm * Zpos c₂)) with (Z.to_nat (mm * Zpos c₂) + 0)%nat by fast_omega. rewrite <- Nat.add_assoc; simpl. rewrite normalise_ps_adjust_add. reflexivity. subst mm; simpl. destruct m; [ reflexivity | simpl ]. apply Pos2Z.is_nonneg. apply Zle_minus_le_0; assumption. subst nn; simpl. destruct n; [ reflexivity | simpl ]. apply Pos2Z.is_nonneg. apply Zle_minus_le_0; assumption. apply Z.nle_gt in H₁. rewrite Z.min_r; [ idtac | apply Z.lt_le_incl; assumption ]. rewrite Z.add_sub_assoc. symmetry. rewrite Z.add_comm. rewrite Z.add_sub_assoc. rewrite Z.add_sub_swap. rewrite <- Z.sub_sub_distr. symmetry. rewrite Z.add_sub_swap. rewrite <- Z.sub_sub_distr. remember (vc₁ - vc₂)%Z as x. rewrite <- Z2Nat.inj_sub. rewrite <- Z2Nat.inj_sub. remember (Z.to_nat (nn * Zpos c₂ - x)) as y. replace y with (y + 0)%nat by fast_omega. rewrite <- Nat.add_assoc; simpl. rewrite normalise_ps_adjust_add. clear y Heqy. remember (Z.to_nat (mm * Zpos c₂ - x)) as y. replace y with (y + 0)%nat by fast_omega. rewrite <- Nat.add_assoc; simpl. rewrite normalise_ps_adjust_add. reflexivity. subst x. apply Zle_minus_le_0, Z.lt_le_incl; assumption. subst x. apply Zle_minus_le_0, Z.lt_le_incl; assumption. rewrite <- Z.sub_max_distr_l, Z.sub_diag. apply Z.le_max_l. rewrite <- Z.sub_max_distr_l, Z.sub_diag. apply Z.le_max_l. rewrite <- Z.sub_max_distr_l, Z.sub_diag. apply Z.le_max_r. subst nn. destruct n; [ reflexivity | simpl ]. apply Pos2Z.is_nonneg. rewrite <- Z.sub_max_distr_l, Z.sub_diag. apply Z.le_max_r. subst mm. destruct m; [ reflexivity | simpl ]. apply Pos2Z.is_nonneg. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add