Mathlib.Algebra.OrderedField.Basic

import Mathlib.Algebra.Ring.Basic

def le.{u} :
  forall (Scalar : Sort u), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (a : Scalar), forall (b : Scalar), Prop :=
  fun Scalar => fun le_rel => fun a => fun b => le_rel a b

def lt.{u} :
  forall (Scalar : Sort u), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (a : Scalar), forall (b : Scalar), Prop :=
  fun Scalar => fun lt_rel => fun a => fun b => lt_rel a b

def sqrt.{u} :
  forall (Scalar : Sort u), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (a : Scalar), Scalar :=
  fun Scalar => fun sqrt_fn => fun a => sqrt_fn a

def Nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (a : Scalar), Prop :=
  fun Scalar => fun zero => fun le_rel => fun a => le_rel zero a

def Positive.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (a : Scalar), Prop :=
  fun Scalar => fun zero => fun lt_rel => fun a => lt_rel zero a

def OrderedFieldLawArgs.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => forall (P : Prop), forall (mk : forall (le_refl_law : forall (a : Scalar), le_rel a a), forall (le_trans_law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c), forall (add_nonneg_law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b)), forall (mul_nonneg_law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b)), forall (square_nonneg_law : forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a)), forall (sqrt_nonneg_law : forall (a : Scalar), le_rel zero (sqrt_fn a)), forall (sqrt_square_of_nonneg_law : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a), forall (sqrt_mul_self_law : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a), forall (eq_of_square_eq_square_nonneg_law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b), forall (add_le_add_law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d)), forall (mul_le_mul_nonneg_law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d)), forall (zero_le_two_law : le_rel zero (@two.{u} Scalar one add)), forall (le_antisymm_law : forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b), forall (lt_of_le_of_ne_law : forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a), forall (le_of_eq_law : forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P), forall (sqrt_sq_law : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a), forall (sq_eq_zero_iff_law : forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R), forall (sum_nonneg_eq_zero_law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R), forall (square_completion_bound_law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hquadratic : forall (t : Scalar), le_rel zero (add (add (mul a (@sq.{u} Scalar mul t)) (mul (mul (@two.{u} Scalar one add) b) t)) c)), le_rel (@sq.{u} Scalar mul b) (mul a c)), forall (le_of_sq_le_sq_nonneg_law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), le_rel a b), forall (le_mul_sqrt_of_sq_le_mul_nonneg_law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul c) (mul a b)), le_rel c (mul (sqrt_fn a) (sqrt_fn b))), forall (add_two_mul_le_sq_add_sqrt_law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (n : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hn : @Eq.{u} Scalar n (add (add a (mul (@two.{u} Scalar one add) c)) b)), forall (hc : le_rel c (mul (sqrt_fn a) (sqrt_fn b))), le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b)))), P), P

theorem le_refl.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), le_rel a a), forall (a : Scalar), le_rel a a :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => law a

theorem le_trans.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun c => fun hab => fun hbc => law a b c hab hbc

theorem add_nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b)), forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun ha => fun hb => law a b ha hb

theorem mul_nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b)), forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun ha => fun hb => law a b ha hb

theorem square_nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a)), forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => law a

theorem sqrt_nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), le_rel zero (sqrt_fn a)), forall (a : Scalar), le_rel zero (sqrt_fn a) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => law a

theorem sqrt_square_of_nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a), forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun ha => law a ha

theorem sqrt_mul_self.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a), forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun ha => law a ha

theorem eq_of_square_eq_square_nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b), forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun ha => fun hb => fun hsq => law a b ha hb hsq

theorem add_le_add.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d)), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun c => fun d => fun hab => fun hcd => law a b c d hab hcd

theorem mul_le_mul_nonneg.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d)), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun c => fun d => fun ha => fun hab => fun hc => fun hcd => law a b c d ha hab hc hcd

theorem zero_le_two.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : le_rel zero (@two.{u} Scalar one add)), le_rel zero (@two.{u} Scalar one add) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => law

theorem le_antisymm.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b), forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun hab => fun hba => law a b hab hba

theorem lt_of_le_of_ne.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a), forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun ha => fun hne => law a ha hne

theorem le_of_eq.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P), forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun hab => fun P => fun mk => law a b hab P mk

theorem sqrt_sq.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a), forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun ha => law a ha

theorem sq_eq_zero_iff.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R), forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun R => fun mk => law a R mk

theorem sum_nonneg_eq_zero.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (law : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R), forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun law => fun a => fun b => fun ha => fun hb => fun hsum => fun R => fun mk => law a b ha hb hsum R mk

theorem square_completion_bound_from_ordered_args.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (ordered_args : @OrderedFieldLawArgs.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hquadratic : forall (t : Scalar), le_rel zero (add (add (mul a (@sq.{u} Scalar mul t)) (mul (mul (@two.{u} Scalar one add) b) t)) c)), le_rel (@sq.{u} Scalar mul b) (mul a c) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun ordered_args => fun a => fun b => fun c => fun hquadratic => ordered_args (le_rel (@sq.{u} Scalar mul b) (mul a c)) (fun (le_refl_arg : forall (a : Scalar), le_rel a a) => fun (le_trans_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c) => fun (add_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b)) => fun (mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b)) => fun (square_nonneg_arg : forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a)) => fun (sqrt_nonneg_arg : forall (a : Scalar), le_rel zero (sqrt_fn a)) => fun (sqrt_square_of_nonneg_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a) => fun (sqrt_mul_self_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a) => fun (eq_of_square_eq_square_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b) => fun (add_le_add_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d)) => fun (mul_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d)) => fun (zero_le_two_arg : le_rel zero (@two.{u} Scalar one add)) => fun (le_antisymm_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b) => fun (lt_of_le_of_ne_arg : forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a) => fun (le_of_eq_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P) => fun (sqrt_sq_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a) => fun (sq_eq_zero_iff_arg : forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R) => fun (sum_nonneg_eq_zero_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R) => fun (square_completion_bound_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hquadratic : forall (t : Scalar), le_rel zero (add (add (mul a (@sq.{u} Scalar mul t)) (mul (mul (@two.{u} Scalar one add) b) t)) c)), le_rel (@sq.{u} Scalar mul b) (mul a c)) => fun (le_of_sq_le_sq_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), le_rel a b) => fun (le_mul_sqrt_of_sq_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul c) (mul a b)), le_rel c (mul (sqrt_fn a) (sqrt_fn b))) => fun (add_two_mul_le_sq_add_sqrt_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (n : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hn : @Eq.{u} Scalar n (add (add a (mul (@two.{u} Scalar one add) c)) b)), forall (hc : le_rel c (mul (sqrt_fn a) (sqrt_fn b))), le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b)))) => square_completion_bound_arg a b c hquadratic)

theorem le_of_sq_le_sq_nonneg_from_ordered_args.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (ordered_args : @OrderedFieldLawArgs.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn), forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), le_rel a b :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun ordered_args => fun a => fun b => fun ha => fun hb => fun hsq => ordered_args (le_rel a b) (fun (le_refl_arg : forall (a : Scalar), le_rel a a) => fun (le_trans_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c) => fun (add_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b)) => fun (mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b)) => fun (square_nonneg_arg : forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a)) => fun (sqrt_nonneg_arg : forall (a : Scalar), le_rel zero (sqrt_fn a)) => fun (sqrt_square_of_nonneg_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a) => fun (sqrt_mul_self_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a) => fun (eq_of_square_eq_square_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b) => fun (add_le_add_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d)) => fun (mul_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d)) => fun (zero_le_two_arg : le_rel zero (@two.{u} Scalar one add)) => fun (le_antisymm_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b) => fun (lt_of_le_of_ne_arg : forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a) => fun (le_of_eq_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P) => fun (sqrt_sq_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a) => fun (sq_eq_zero_iff_arg : forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R) => fun (sum_nonneg_eq_zero_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R) => fun (square_completion_bound_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hquadratic : forall (t : Scalar), le_rel zero (add (add (mul a (@sq.{u} Scalar mul t)) (mul (mul (@two.{u} Scalar one add) b) t)) c)), le_rel (@sq.{u} Scalar mul b) (mul a c)) => fun (le_of_sq_le_sq_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), le_rel a b) => fun (le_mul_sqrt_of_sq_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul c) (mul a b)), le_rel c (mul (sqrt_fn a) (sqrt_fn b))) => fun (add_two_mul_le_sq_add_sqrt_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (n : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hn : @Eq.{u} Scalar n (add (add a (mul (@two.{u} Scalar one add) c)) b)), forall (hc : le_rel c (mul (sqrt_fn a) (sqrt_fn b))), le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b)))) => le_of_sq_le_sq_nonneg_arg a b ha hb hsq)

theorem add_dist_nonneg_from_ordered_args.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (ordered_args : @OrderedFieldLawArgs.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn), forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun ordered_args => fun a => fun b => fun ha => fun hb => ordered_args (le_rel zero (add a b)) (fun (le_refl_arg : forall (a : Scalar), le_rel a a) => fun (le_trans_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c) => fun (add_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b)) => fun (mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b)) => fun (square_nonneg_arg : forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a)) => fun (sqrt_nonneg_arg : forall (a : Scalar), le_rel zero (sqrt_fn a)) => fun (sqrt_square_of_nonneg_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a) => fun (sqrt_mul_self_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a) => fun (eq_of_square_eq_square_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b) => fun (add_le_add_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d)) => fun (mul_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d)) => fun (zero_le_two_arg : le_rel zero (@two.{u} Scalar one add)) => fun (le_antisymm_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b) => fun (lt_of_le_of_ne_arg : forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a) => fun (le_of_eq_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P) => fun (sqrt_sq_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a) => fun (sq_eq_zero_iff_arg : forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R) => fun (sum_nonneg_eq_zero_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R) => fun (square_completion_bound_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hquadratic : forall (t : Scalar), le_rel zero (add (add (mul a (@sq.{u} Scalar mul t)) (mul (mul (@two.{u} Scalar one add) b) t)) c)), le_rel (@sq.{u} Scalar mul b) (mul a c)) => fun (le_of_sq_le_sq_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), le_rel a b) => fun (le_mul_sqrt_of_sq_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul c) (mul a b)), le_rel c (mul (sqrt_fn a) (sqrt_fn b))) => fun (add_two_mul_le_sq_add_sqrt_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (n : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hn : @Eq.{u} Scalar n (add (add a (mul (@two.{u} Scalar one add) c)) b)), forall (hc : le_rel c (mul (sqrt_fn a) (sqrt_fn b))), le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b)))) => add_nonneg_arg a b ha hb)

theorem sqrt_sum_square_bound_from_ordered_args.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (ordered_args : @OrderedFieldLawArgs.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hc : le_rel zero c), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul (add b c))), le_rel a (add b c) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun ordered_args => fun a => fun b => fun c => fun ha => fun hb => fun hc => fun hsq => @le_of_sq_le_sq_nonneg_from_ordered_args.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn ordered_args a (add b c) ha (@add_dist_nonneg_from_ordered_args.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn ordered_args b c hb hc) hsq

theorem le_mul_sqrt_of_sq_le_mul_nonneg_from_ordered_args.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (ordered_args : @OrderedFieldLawArgs.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul c) (mul a b)), le_rel c (mul (sqrt_fn a) (sqrt_fn b)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun ordered_args => fun a => fun b => fun c => fun ha => fun hb => fun hsq => ordered_args (le_rel c (mul (sqrt_fn a) (sqrt_fn b))) (fun (le_refl_arg : forall (a : Scalar), le_rel a a) => fun (le_trans_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c) => fun (add_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b)) => fun (mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b)) => fun (square_nonneg_arg : forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a)) => fun (sqrt_nonneg_arg : forall (a : Scalar), le_rel zero (sqrt_fn a)) => fun (sqrt_square_of_nonneg_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a) => fun (sqrt_mul_self_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a) => fun (eq_of_square_eq_square_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b) => fun (add_le_add_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d)) => fun (mul_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d)) => fun (zero_le_two_arg : le_rel zero (@two.{u} Scalar one add)) => fun (le_antisymm_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b) => fun (lt_of_le_of_ne_arg : forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a) => fun (le_of_eq_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P) => fun (sqrt_sq_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a) => fun (sq_eq_zero_iff_arg : forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R) => fun (sum_nonneg_eq_zero_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R) => fun (square_completion_bound_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hquadratic : forall (t : Scalar), le_rel zero (add (add (mul a (@sq.{u} Scalar mul t)) (mul (mul (@two.{u} Scalar one add) b) t)) c)), le_rel (@sq.{u} Scalar mul b) (mul a c)) => fun (le_of_sq_le_sq_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), le_rel a b) => fun (le_mul_sqrt_of_sq_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul c) (mul a b)), le_rel c (mul (sqrt_fn a) (sqrt_fn b))) => fun (add_two_mul_le_sq_add_sqrt_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (n : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hn : @Eq.{u} Scalar n (add (add a (mul (@two.{u} Scalar one add) c)) b)), forall (hc : le_rel c (mul (sqrt_fn a) (sqrt_fn b))), le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b)))) => le_mul_sqrt_of_sq_le_mul_nonneg_arg a b c ha hb hsq)

theorem add_two_mul_le_sq_add_sqrt_from_ordered_args.{u} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (lt_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (ordered_args : @OrderedFieldLawArgs.{u} Scalar zero one add neg sub mul le_rel lt_rel sqrt_fn), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (n : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hn : @Eq.{u} Scalar n (add (add a (mul (@two.{u} Scalar one add) c)) b)), forall (hc : le_rel c (mul (sqrt_fn a) (sqrt_fn b))), le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b))) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun lt_rel => fun sqrt_fn => fun ordered_args => fun a => fun b => fun c => fun n => fun ha => fun hb => fun hn => fun hc => ordered_args (le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b)))) (fun (le_refl_arg : forall (a : Scalar), le_rel a a) => fun (le_trans_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hab : le_rel a b), forall (hbc : le_rel b c), le_rel a c) => fun (add_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (add a b)) => fun (mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), le_rel zero (mul a b)) => fun (square_nonneg_arg : forall (a : Scalar), le_rel zero (@sq.{u} Scalar mul a)) => fun (sqrt_nonneg_arg : forall (a : Scalar), le_rel zero (sqrt_fn a)) => fun (sqrt_square_of_nonneg_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (@sq.{u} Scalar mul a)) a) => fun (sqrt_mul_self_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (sqrt_fn (mul a a)) a) => fun (eq_of_square_eq_square_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), @Eq.{u} Scalar a b) => fun (add_le_add_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (hab : le_rel a b), forall (hcd : le_rel c d), le_rel (add a c) (add b d)) => fun (mul_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), forall (ha : le_rel zero a), forall (hab : le_rel a b), forall (hc : le_rel zero c), forall (hcd : le_rel c d), le_rel (mul a c) (mul b d)) => fun (zero_le_two_arg : le_rel zero (@two.{u} Scalar one add)) => fun (le_antisymm_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : le_rel a b), forall (hba : le_rel b a), @Eq.{u} Scalar a b) => fun (lt_of_le_of_ne_arg : forall (a : Scalar), forall (ha : le_rel zero a), forall (hne : forall (haz : @Eq.{u} Scalar a zero), forall (P : Prop), P), lt_rel zero a) => fun (le_of_eq_arg : forall (a : Scalar), forall (b : Scalar), forall (hab : @Eq.{u} Scalar a b), forall (P : Prop), forall (mk : forall (hab_le : le_rel a b), forall (hba_le : le_rel b a), P), P) => fun (sqrt_sq_arg : forall (a : Scalar), forall (ha : le_rel zero a), @Eq.{u} Scalar (@sq.{u} Scalar mul (sqrt_fn a)) a) => fun (sq_eq_zero_iff_arg : forall (a : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsqz : @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), @Eq.{u} Scalar a zero), forall (backward : forall (haz : @Eq.{u} Scalar a zero), @Eq.{u} Scalar (@sq.{u} Scalar mul a) zero), R), R) => fun (sum_nonneg_eq_zero_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsum : @Eq.{u} Scalar (add a b) zero), forall (R : Prop), forall (mk : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), R), R) => fun (square_completion_bound_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (hquadratic : forall (t : Scalar), le_rel zero (add (add (mul a (@sq.{u} Scalar mul t)) (mul (mul (@two.{u} Scalar one add) b) t)) c)), le_rel (@sq.{u} Scalar mul b) (mul a c)) => fun (le_of_sq_le_sq_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), le_rel a b) => fun (le_mul_sqrt_of_sq_le_mul_nonneg_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hsq : le_rel (@sq.{u} Scalar mul c) (mul a b)), le_rel c (mul (sqrt_fn a) (sqrt_fn b))) => fun (add_two_mul_le_sq_add_sqrt_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (n : Scalar), forall (ha : le_rel zero a), forall (hb : le_rel zero b), forall (hn : @Eq.{u} Scalar n (add (add a (mul (@two.{u} Scalar one add) c)) b)), forall (hc : le_rel c (mul (sqrt_fn a) (sqrt_fn b))), le_rel n (@sq.{u} Scalar mul (add (sqrt_fn a) (sqrt_fn b)))) => add_two_mul_le_sq_add_sqrt_arg a b c n ha hb hn hc)