proposition: Lemma Rlt_1_mult_inv : forall x y, 0 < y -> y < x -> 1 < x * / y.
proof: Proof. intros x y y_pos y_lb ; apply Rle_lt_trans with (y * / y). right ; symmetry ; apply Rinv_r ; apply Rgt_not_eq ; assumption. apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat |] ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra