import Mathlib.Tactic
variable {α : Type _} [CommRing α]
variable {x y : α}

-- (suma_de_cuadrados x) afirma que x se puede escribir como la suma
-- de dos cuadrados.
def suma_de_cuadrados (x : α) :=
  ∃ a b, x = a^2 + b^2

example
  (hx : suma_de_cuadrados x)
  (hy : suma_de_cuadrados y)
  : suma_de_cuadrados (x * y) :=
by sorry

import src.Cota_superior_de_producto_por_escalar

variable {f : ℝ → ℝ}
variable {c : ℝ}

-- (acotadaSup f) afirma que f tiene cota superior.
def acotadaSup (f : ℝ → ℝ) :=
  ∃ a, CotaSuperior f a

example
  (hf : acotadaSup f)
  (hc : c ≥ 0)
  : acotadaSup (fun x ↦ c * f x) :=
by sorry

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.
def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

variable {f : ℝ → ℝ}
variable {c : ℝ}

example
  (hfa : CotaSuperior f a)
  (h : c ≥ 0)
  : CotaSuperior (fun x ↦ c * f x) (c * a) :=
by sorry

import src.Suma_de_cotas_inferiores
variable {f g : ℝ → ℝ}

-- (acotadaInf f) afirma que f tiene cota inferior.
def acotadaInf (f : ℝ → ℝ) :=
  ∃ a, CotaInferior f a

example
  (hf : acotadaInf f)
  (hg : acotadaInf g)
  : acotadaInf (f + g) :=
by sorry

import src.Suma_de_cotas_superiores
variable {f g : ℝ → ℝ}

-- (acotadaSup f) afirma que f tiene cota superior.
def acotadaSup (f : ℝ → ℝ) :=
  ∃ a, CotaSuperior f a

example
  (hf : acotadaSup f)
  (hg : acotadaSup g)
  : acotadaSup (f + g) :=
by sorry

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
by sorry

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by sorry

import Mathlib.Data.Real.Basic
open Function
variable {c : ℝ}

example
  (h : c ≠ 0)
  : Injective ((c * .)) :=
by sorry

import Mathlib.Data.Real.Basic
open Function

variable {c : ℝ}

example : Injective ((. + c)) :=
by sorry

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (s : Set α)
variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.
def CotaSupConj (s : Set α) (a : α) :=
  ∀ {x}, x ∈ s → x ≤ a

example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by sorry