proposition: Lemma low_bd_set_opp_to_upp_bd_set : ∀ (A : ℝ → Prop) (m : ℝ), is_lower_bound (set_opp A) m ⇒ -m is an upper bound for A.
proof: Proof. Take A : (ℝ → Prop) and m : ℝ. Assume that (is_lower_bound (set_opp A) m). We need to show that (∀ a : ℝ, (A a) ⇒ a ≤ -m). Take a : ℝ. Assume that (A a). It holds that (for all b : ℝ, (set_opp A b) ⇒ m ≤ b). We claim that (A (--a)). { It holds that (--a = a) (ii). It holds that (A a) (iii). exact (eq_ind_r(_,_,A,(iii),_,(ii))). } It holds that ((set_opp A) (-a)). Define b := (-a). It holds that (m ≤ b). It holds that (m ≤ -a). We conclude that (a ≤ - m). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics