proposition: Lemma rle_diffP a b: realp a -> realp b -> (a <=r b <-> inc (b -r a) BRp).
proof: Proof. move => ar br. move:(iff_sym (BRsum_le2r ar br (RSo ar))); rewrite (BRsum_opp_r ar) => h. apply: (iff_trans h); apply/rle0xP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)