proposition: Lemma rle_diffP1 a b: realp a -> realp b -> (a <=r b <-> \0r <=r (b -r a)).
proof: Proof. move => ar br; apply: (iff_trans (rle_diffP ar br)). apply: iff_sym; exact:rle0xP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)