proposition: Lemma lee_addgt0Pr x y : reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).
proof: Proof. apply/(iffP idP) => [|]. - move: x y => [x| |] [y| |]//. + by rewrite lee_fin => xy e e0; rewrite -EFinD lee_fin ler_wpDr// ltW. + by move=> _ e e0; rewrite leNye. - move: x y => [x| |] [y| |]// xy; rewrite ?leey ?leNye//; [|by move: xy => /(_ _ lte01)..]. by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed