proposition: Theorem Rle_Rinv : forall x y : R, (0 < x)%R -> (x <= y)%R -> (/ y <= / x)%R.
proof: Proof. intros x y H H1; case H1; intros H2. left; apply Rinv_lt_contravar; auto. apply Rmult_lt_0_compat; auto. apply Rlt_trans with (2 := H2); auto. rewrite H2; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz