proposition: Lemma lee_daddgt0Pr x y : reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).
proof: Proof. exact: lee_addgt0Pr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed