proposition: Lemma bdd_below_to_bdd_above_set_opp : ∀ (A : ℝ → Prop), is_bounded_below A ⇒ is_bounded_above (set_opp A).
proof: Proof. Take A : (ℝ → Prop). Assume that (is_bounded_below A) (i). We need to show that (∃ M : ℝ, is_upper_bound (set_opp A) M). By (i) it holds that (there exists m : ℝ, is_lower_bound A m). Obtain such an m. Choose M := (-m). By low_bd_set_to_upp_bd_set_opp we conclude that (is_upper_bound (set_opp A) (M)). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics