proposition: Lemma sup_is_upp_bd : ∀ A : (ℝ → Prop), ∀ M : ℝ, is_sup A M ⇒ is_upper_bound A M.
proof: Proof. Take A : (ℝ → Prop). Take M : ℝ. Assume that (is_sup A M). It holds that (is_upper_bound A M ∧ (for all b : ℝ, is_upper_bound A b ⇨ M ≤ b)) (i). Because (i) both (is_upper_bound A M) and (for all M0 : ℝ, is_upper_bound A M0 ⇨ M ≤ M0) hold. It follows that (is_upper_bound A M). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics