proposition: Theorem normalise_ps_add_adjust_l : ∀ ps₁ ps₂ n k, normalise_ps (ps₁ + ps₂)%ps ≐ normalise_ps (adjust_ps n k ps₁ + ps₂)%ps.
proof: Proof. intros ps₁ ps₂ n k. rewrite eq_strong_ps_add_adjust_0_l with (k := k). apply normalise_ps_add_adjust. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add