[STATEMENT]
lemma pos_minus_divideR_le_eq [field_simps]:
  "- (b /\<^sub>R c) \<le> a \<longleftrightarrow> - b \<le> c *\<^sub>R a" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (b /\<^sub>R c) \<le> a) = (- b \<le> c *\<^sub>R a)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. (- (b /\<^sub>R c) \<le> a) = (- b \<le> c *\<^sub>R a)
[PROOF STEP]
by (metis pos_divideR_le_eq pos_le_minus_divideR_eq that
    inverse_positive_iff_positive le_imp_neg_le minus_minus)