proposition: Lemma ler_addgt0Pr x y : reflect (forall e, e > 0 -> x <= y + e) (x <= y).
proof: Proof. apply/(iffP idP)=> [lexy e e_gt0 | lexye]; first by rewrite ler_wpDr// ltW. have [||ltyx]// := comparable_leP. rewrite (@comparabler_trans _ (y + 1))// /Order.comparable ?lexye ?ltr01//. by rewrite lerDl ler01 orbT. have /midf_lt [_] := ltyx; rewrite le_gtF//. rewrite -(@addrK _ y y) (addrAC _ _ x) -addrA 2!mulrDl -splitr lexye//. by rewrite divr_gt0// ?ltr0n// subr_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)