proposition: Lemma inv_remove : forall r1 r2 : R, 0 < r1 -> 0 < r2 -> 1 / r1 < 1 / r2 -> r1 > r2.
proof: Proof. intros. unfold Rdiv in *. rewrite Rmult_1_l in *. rewrite <- (Rinv_inv r1), <- (Rinv_inv r2). apply (Rinv_lt_contravar (/ r1) (/ r2)). apply Rmult_lt_0_compat. apply Rinv_0_lt_compat. apply H. apply Rinv_0_lt_compat. apply H0. rewrite Rmult_1_l in *. apply H1. all: apply Rgt_not_eq; assumption. Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations