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