proposition: Lemma BRdiff_le1P a b c: realp a -> realp b -> realp c -> (a -r b <=r c <-> a -r c <=r b).
proof: Proof. move => ar br cr. move: (BRsum_le2r (RS_diff ar br) cr br). rewrite (BRsum_diff1 br ar) => ha. move: (BRsum_le2r (RS_diff ar cr) br cr). rewrite (BRsum_diff1 cr ar) BRsumC => hb. exact: (iff_trans (iff_sym ha) hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)