proposition: Theorem gcd_ps_0_m : ∀ n (ps : puiseux_series α), gcd_ps n O ps = Z.abs (Z.gcd (ps_ordnum ps + Z.of_nat n) (Zpos (ps_polydo ps))).
proof: Proof. intros n ps. unfold gcd_ps. rewrite Z.gcd_0_r; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series