proposition: Lemma Rinv_lt_contravar_rev : forall x y, 0 < x -> 0 < y -> /x < /y -> y < x.
proof: Proof. intros x y x_pos y_pos Hxy ; rewrite <- (Rinv_inv x), <- (Rinv_inv y) ; try (apply Rgt_not_eq ; assumption). apply Rinv_lt_contravar ; [| assumption] ; apply Rmult_lt_0_compat ; apply Rinv_0_lt_compat ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra