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