proposition: Lemma rlt_diffP2 a b: realp a -> realp b -> (a <r b <-> inc (a -r b) BRms).
proof: Proof. move => ar br; apply: (iff_trans (rlt_diffP ar br)). rewrite - (BRoppB br ar); split => h; first by apply: BRopp_positive1. rewrite - (BRopp_K (RS_diff br ar)); apply: (BRopp_negative1 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)