Mathlib.Algebra.OrderedField.Square

import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.OrderedField.Basic

theorem square_def.{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 (a : Scalar), @Eq.{u} Scalar (@sq.{u} Scalar mul a) (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 a => @Eq.refl.{u} Scalar (@sq.{u} Scalar mul a)

theorem mul_self_eq_square.{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 (a : Scalar), @Eq.{u} Scalar (mul a a) (@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 a => @Eq.refl.{u} Scalar (mul a a)

theorem sq_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), @Eq.{u} Scalar (@sq.{u} Scalar mul (add a b)) (add (add (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul b))), forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (@sq.{u} Scalar mul (add a b)) (add (add (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul 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 => law a b

theorem sq_sub.{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), @Eq.{u} Scalar (@sq.{u} Scalar mul (sub a b)) (add (sub (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul b))), forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (@sq.{u} Scalar mul (sub a b)) (add (sub (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul 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 => law a b

theorem sum_two_squares_comm.{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 (x : Scalar), forall (y : Scalar), @Eq.{u} Scalar (add x y) (add y x)), forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)) (add (@sq.{u} Scalar mul b) (@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 => fun b => law (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)

theorem cancel_double_zero_term.{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 (x : Scalar), forall (hzero : @Eq.{u} Scalar x zero), @Eq.{u} Scalar (add a (mul (@two.{u} Scalar one add) x)) a), forall (a : Scalar), forall (x : Scalar), forall (hzero : @Eq.{u} Scalar x zero), @Eq.{u} Scalar (add a (mul (@two.{u} Scalar one add) x)) 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 x => fun hzero => law a x hzero

theorem sq_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), @Eq.{u} Scalar (mul a zero) zero), @Eq.{u} Scalar (@sq.{u} Scalar mul zero) zero :=
  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 zero

theorem sq_one.{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), @Eq.{u} Scalar (mul a one) a), @Eq.{u} Scalar (@sq.{u} Scalar mul one) one :=
  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 one

theorem sq_neg.{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), @Eq.{u} Scalar (mul (neg a) (neg a)) (mul a a)), forall (a : Scalar), @Eq.{u} Scalar (@sq.{u} Scalar mul (neg a)) (@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 two_mul.{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), @Eq.{u} Scalar (mul (@two.{u} Scalar one add) a) (add a a)), forall (a : Scalar), @Eq.{u} Scalar (mul (@two.{u} Scalar one add) a) (add 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 sq_eq_sq_of_eq_or_neg_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 (h : forall (R : Prop), forall (eq_case : forall (hab : @Eq.{u} Scalar a b), R), forall (neg_case : forall (hanb : @Eq.{u} Scalar a (neg b)), R), R), @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)), forall (a : Scalar), forall (b : Scalar), forall (h : forall (R : Prop), forall (eq_case : forall (hab : @Eq.{u} Scalar a b), R), forall (neg_case : forall (hanb : @Eq.{u} Scalar a (neg b)), R), R), @Eq.{u} Scalar (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul 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 h => law a b h

theorem sq_add_eq_add_sq_add_two_mul.{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), @Eq.{u} Scalar (@sq.{u} Scalar mul (add a b)) (add (add (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul b))), forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (@sq.{u} Scalar mul (add a b)) (add (add (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul 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 => law a b

theorem sq_sub_eq_add_sq_sub_two_mul.{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), @Eq.{u} Scalar (@sq.{u} Scalar mul (sub a b)) (add (sub (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul b))), forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (@sq.{u} Scalar mul (sub a b)) (add (sub (@sq.{u} Scalar mul a) (mul (mul (@two.{u} Scalar one add) a) b)) (@sq.{u} Scalar mul 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 => law a b

theorem add_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 (b : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsum : @Eq.{u} Scalar (add (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)) zero), forall (S : Prop), forall (mk_pair : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), S), S), forall (backward : forall (hpair : forall (S : Prop), forall (mk_pair : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), S), S), @Eq.{u} Scalar (add (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)) zero), R), R), forall (a : Scalar), forall (b : Scalar), forall (R : Prop), forall (mk : forall (forward : forall (hsum : @Eq.{u} Scalar (add (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul b)) zero), forall (S : Prop), forall (mk_pair : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), S), S), forall (backward : forall (hpair : forall (S : Prop), forall (mk_pair : forall (haz : @Eq.{u} Scalar a zero), forall (hbz : @Eq.{u} Scalar b zero), S), S), @Eq.{u} Scalar (add (@sq.{u} Scalar mul a) (@sq.{u} Scalar mul 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 R => fun mk => law a b R mk

theorem mul_two_zero_term.{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 (x : Scalar), forall (hzero : @Eq.{u} Scalar x zero), @Eq.{u} Scalar (mul (@two.{u} Scalar one add) x) zero), forall (x : Scalar), forall (hzero : @Eq.{u} Scalar x zero), @Eq.{u} Scalar (mul (@two.{u} Scalar one add) x) zero :=
  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 x => fun hzero => law x hzero

theorem normalize_add_with_zero_cross_term.{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 (x : Scalar), forall (hzero : @Eq.{u} Scalar x zero), @Eq.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) x)) b) (add a b)), forall (a : Scalar), forall (b : Scalar), forall (x : Scalar), forall (hzero : @Eq.{u} Scalar x zero), @Eq.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) x)) b) (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 x => fun hzero => law a b x hzero