proposition: Lemma Rbar_abs_lt_between (x y : Rbar) : Rbar_lt (Rbar_abs x) y <-> (Rbar_lt (Rbar_opp y) x /\ Rbar_lt x y).
proof: Proof. case: x => [x | | ] ; case: y => [y | | ] /= ; try by intuition. by apply Rabs_lt_between. Qed.
imports: Coq(Reals ssreflect) Rcomplements