proposition: Lemma cut_epsilon {R : archiFieldType} (eps : R) : (0 < eps)%R -> exists eps1 eps2 : R, [/\ (0 < eps1)%R, (0 < eps2)%R, (eps1 + eps2 <= eps)%R, eps1 < eps & eps2 < eps].
proof: Proof. move=> p; exists (eps / 2%:R), (eps / 2%:R). have p1 : (0 < eps / 2%:R)%R by rewrite divr_gt0// ltr0n. have cmp : eps / 2%:R < eps. by rewrite ltr_pdivr_mulr// ?ltr0n// ltr_pmulr// ltr1n. split => //. by rewrite -mulrDr ger_pmulr// -mulr2n -mulr_natr mulVf// pnatr_eq0. Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc