proposition: Theorem Rinv_lt : forall x y, (0 < x)%R -> (x < y)%R -> (/y < /x)%R.
proof: Proof. intros x y Hx Hxy. apply Rinv_lt_contravar. apply Rmult_lt_0_compat. exact Hx. now apply Rlt_trans with x. exact Hxy. Qed.
imports: Coq(Psatz Reals ZArith) Zaux