proposition: Lemma rlt_diffP a b: realp a -> realp b -> (a <r b <-> inc (b -r a) BRps).
proof: Proof. move => ar br; split. move => [] /(rle_diffP ar br) => pc pd; apply /BRps_iP;split => //. dneg aux; symmetry; exact (BRdiff_xx_rw br ar aux). move /BRps_iP => [] /(rle_diffP ar br) pc pd; split => //. by dneg aux; rewrite aux (BRdiff_xx br). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)