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