proposition: Lemma low_bd_set_to_upp_bd_set_opp : ∀ (A : ℝ → Prop) (m : ℝ), is_lower_bound A m ⇒ -m is an upper bound for (set_opp A).
proof: Proof. Take A : (ℝ → Prop) and m : ℝ. Assume that (is_lower_bound A m) (i). We need to show that (for all b : ℝ, (set_opp A b) ⇒ b ≤ -m). Take b : ℝ. Assume that (set_opp A b). Define a := (-b). By (i) it holds that (m ≤ a). We conclude that (& b = -a <= -m). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics