proposition: Lemma upp_bd_set_opp_to_low_bd_set : ∀ (A : ℝ → Prop) (M : ℝ), is_upper_bound (set_opp A) M ⇒ is_lower_bound A (-M).
proof: Proof. Take A : (ℝ → Prop) and M : ℝ. Assume that (is_upper_bound (set_opp A) M) (i). We need to show that (∀ a : ℝ, (A a) ⇒ -M ≤ a). Take a : ℝ. Assume that (A a). 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). By (i) it holds that (b ≤ M). It holds that (-a ≤ M). We conclude that (- M ≤ a). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics