proposition: Lemma rle_diffP2 a b: realp a -> realp b -> (a <=r b <-> inc (a -r b) BRm).
proof: Proof. move => ar br; apply: (iff_trans (rle_diffP ar br)). rewrite - (BRoppB br ar); split => h; first by apply: BRopp_positive2. rewrite - (BRopp_K (RS_diff br ar)); apply: (BRopp_negative2 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)