proposition: Lemma Rbar_div_pos_lt (x y : Rbar) (z : posreal) : Rbar_lt x y <-> Rbar_lt (Rbar_div_pos x z) (Rbar_div_pos y z).
proof: Proof. case: z => z Hz ; case: x => [x | | ] ; case: y => [y | | ] ; split => //= H. apply (Rmult_lt_compat_r (/z)) => // ; by apply Rinv_0_lt_compat. apply (Rmult_lt_reg_r (/z)) => // ; by apply Rinv_0_lt_compat. Qed.
imports: Coq(Reals ssreflect) Rcomplements