proposition: Lemma Rleb_def x y : (Rleb x y) = (Rabs (y - x) == y - x).
proof: Proof. apply/(sameP (RlebP x y))/(iffP idP)=> [/eqP H| /Rle_minus H]. apply: Rminus_le; rewrite -Ropp_minus_distr. apply/Rge_le/Ropp_0_le_ge_contravar. by rewrite -H; apply: Rabs_pos. apply/eqP/Rabs_pos_eq. rewrite -Ropp_minus_distr. by apply/Ropp_0_ge_le_contravar/Rle_ge. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures)