Mathlib.Algebra.OrderedField.ScalarIdentities

import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.OrderedField.Square
import Mathlib.Logic.EqReasoning

theorem mul_two_zero_term_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), 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 ring_args => fun x => fun hzero => ring_args (@Eq.{u} Scalar (mul (@two.{u} Scalar one add) x) zero) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @Eq.rec.{u,0} Scalar zero (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar zero y) => @Eq.{u} Scalar (mul (@two.{u} Scalar one add) y) zero) (mul_zero_arg (@two.{u} Scalar one add)) x (@Eq.rec.{u,0} Scalar x (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar x y) => @Eq.{u} Scalar y x) (@Eq.refl.{u} Scalar x) zero hzero))

theorem cancel_double_zero_term_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), 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 ring_args => fun a => fun x => fun hzero => ring_args (@Eq.{u} Scalar (add a (mul (@two.{u} Scalar one add) x)) a) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @Eq.rec.{u,0} Scalar zero (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar zero y) => @Eq.{u} Scalar (add a y) a) (add_zero_arg a) (mul (@two.{u} Scalar one add) x) (@Eq.rec.{u,0} Scalar (mul (@two.{u} Scalar one add) x) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (mul (@two.{u} Scalar one add) x) y) => @Eq.{u} Scalar y (mul (@two.{u} Scalar one add) x)) (@Eq.refl.{u} Scalar (mul (@two.{u} Scalar one add) x)) zero (@mul_two_zero_term_from_ring_args.{u} Scalar zero one add neg sub mul ring_args x hzero)))

theorem normalize_add_with_zero_cross_term_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), 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 ring_args => fun a => fun b => fun x => fun hzero => @Eq.rec.{u,0} Scalar (add a (mul (@two.{u} Scalar one add) x)) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add a (mul (@two.{u} Scalar one add) x)) y) => @Eq.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) x)) b) (add y b)) (@Eq.refl.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) x)) b)) a (@cancel_double_zero_term_from_ring_args.{u} Scalar zero one add neg sub mul ring_args a x hzero)

theorem mul_two_neg_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (x : Scalar), @Eq.{u} Scalar (mul (@two.{u} Scalar one add) (neg x)) (neg (mul (@two.{u} Scalar one add) x)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun x => ring_args (@Eq.{u} Scalar (mul (@two.{u} Scalar one add) (neg x)) (neg (mul (@two.{u} Scalar one add) x))) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => add_left_cancel_arg (mul (@two.{u} Scalar one add) x) (mul (@two.{u} Scalar one add) (neg x)) (neg (mul (@two.{u} Scalar one add) x)) (@Eq.rec.{u,0} Scalar zero (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar zero y) => @Eq.{u} Scalar (add (mul (@two.{u} Scalar one add) x) (mul (@two.{u} Scalar one add) (neg x))) y) (@Eq.rec.{u,0} Scalar (mul (@two.{u} Scalar one add) (add x (neg x))) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (mul (@two.{u} Scalar one add) (add x (neg x))) y) => @Eq.{u} Scalar y zero) (@Eq.rec.{u,0} Scalar (mul (@two.{u} Scalar one add) zero) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (mul (@two.{u} Scalar one add) zero) y) => @Eq.{u} Scalar (mul (@two.{u} Scalar one add) (add x (neg x))) y) (@Eq.rec.{u,0} Scalar (add x (neg x)) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add x (neg x)) y) => @Eq.{u} Scalar (mul (@two.{u} Scalar one add) (add x (neg x))) (mul (@two.{u} Scalar one add) y)) (@Eq.refl.{u} Scalar (mul (@two.{u} Scalar one add) (add x (neg x)))) zero (add_neg_cancel_arg x)) zero (mul_zero_arg (@two.{u} Scalar one add))) (add (mul (@two.{u} Scalar one add) x) (mul (@two.{u} Scalar one add) (neg x))) (left_distrib_arg (@two.{u} Scalar one add) x (neg x))) (add (mul (@two.{u} Scalar one add) x) (neg (mul (@two.{u} Scalar one add) x))) (@Eq.rec.{u,0} Scalar (add (mul (@two.{u} Scalar one add) x) (neg (mul (@two.{u} Scalar one add) x))) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add (mul (@two.{u} Scalar one add) x) (neg (mul (@two.{u} Scalar one add) x))) y) => @Eq.{u} Scalar y (add (mul (@two.{u} Scalar one add) x) (neg (mul (@two.{u} Scalar one add) x)))) (@Eq.refl.{u} Scalar (add (mul (@two.{u} Scalar one add) x) (neg (mul (@two.{u} Scalar one add) x)))) zero (add_neg_cancel_arg (mul (@two.{u} Scalar one add) x)))))

theorem add_neg_cross_term_to_sub_sum_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (a : Scalar), forall (b : Scalar), forall (t : Scalar), @Eq.{u} Scalar (add (add a (neg t)) b) (sub (add a b) t) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun a => fun b => fun t => ring_args (@Eq.{u} Scalar (add (add a (neg t)) b) (sub (add a b) t)) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @Eq.rec.{u,0} Scalar (add a (add (neg t) b)) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add a (add (neg t) b)) y) => @Eq.{u} Scalar (add (add a (neg t)) b) y) (add_assoc_arg a (neg t) b) (sub (add a b) t) (@Eq.rec.{u,0} Scalar (add a (add b (neg t))) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add a (add b (neg t))) y) => @Eq.{u} Scalar (add a (add (neg t) b)) y) (@Eq.rec.{u,0} Scalar (add (neg t) b) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add (neg t) b) y) => @Eq.{u} Scalar (add a (add (neg t) b)) (add a y)) (@Eq.refl.{u} Scalar (add a (add (neg t) b))) (add b (neg t)) (add_comm_arg (neg t) b)) (sub (add a b) t) (@Eq.rec.{u,0} Scalar (add (add a b) (neg t)) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add (add a b) (neg t)) y) => @Eq.{u} Scalar (add a (add b (neg t))) y) (@Eq.rec.{u,0} Scalar (add (add a b) (neg t)) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add (add a b) (neg t)) y) => @Eq.{u} Scalar y (add (add a b) (neg t))) (@Eq.refl.{u} Scalar (add (add a b) (neg t))) (add a (add b (neg t))) (add_assoc_arg a b (neg t))) (sub (add a b) t) (@Eq.rec.{u,0} Scalar (sub (add a b) t) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (sub (add a b) t) y) => @Eq.{u} Scalar y (sub (add a b) t)) (@Eq.refl.{u} Scalar (sub (add a b) t)) (add (add a b) (neg t)) (sub_eq_add_neg_arg (add a b) t)))))

theorem law_of_cosines_scalar_rhs_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (a : Scalar), forall (b : Scalar), forall (x : Scalar), @Eq.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) (neg x))) b) (sub (add a b) (mul (@two.{u} Scalar one add) x)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun a => fun b => fun x => @Eq.rec.{u,0} Scalar (add (add a (neg (mul (@two.{u} Scalar one add) x))) b) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (add (add a (neg (mul (@two.{u} Scalar one add) x))) b) y) => @Eq.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) (neg x))) b) y) (@Eq.rec.{u,0} Scalar (mul (@two.{u} Scalar one add) (neg x)) (fun (y : Scalar) => fun (hy : @Eq.{u} Scalar (mul (@two.{u} Scalar one add) (neg x)) y) => @Eq.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) (neg x))) b) (add (add a y) b)) (@Eq.refl.{u} Scalar (add (add a (mul (@two.{u} Scalar one add) (neg x))) b)) (neg (mul (@two.{u} Scalar one add) x)) (@mul_two_neg_from_ring_args.{u} Scalar zero one add neg sub mul ring_args x)) (sub (add a b) (mul (@two.{u} Scalar one add) x)) (@add_neg_cross_term_to_sub_sum_from_ring_args.{u} Scalar zero one add neg sub mul ring_args a b (mul (@two.{u} Scalar one add) x))

theorem two_mul_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), 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 ring_args => fun a => ring_args (@Eq.{u} Scalar (mul (@two.{u} Scalar one add) a) (add a a)) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @eq_trans.{u} Scalar (mul (@two.{u} Scalar one add) a) (add (mul one a) (mul one a)) (add a a) (right_distrib_arg one one a) (@eq_congr2.{u,u,u} Scalar Scalar Scalar add (mul one a) a (mul one a) a (one_mul_arg a) (one_mul_arg a)))

theorem add_sub_cross_cancel_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (a : Scalar), forall (x : Scalar), @Eq.{u} Scalar (add x (sub a x)) a :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun a => fun x => ring_args (@Eq.{u} Scalar (add x (sub a x)) a) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @eq_trans.{u} Scalar (add x (sub a x)) (add (sub a x) x) a (add_comm_arg x (sub a x)) (sub_add_cancel_arg a x))

theorem add_pairwise_commute_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (d : Scalar), @Eq.{u} Scalar (add (add a b) (add c d)) (add (add a c) (add b d)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun a => fun b => fun c => fun d => ring_args (@Eq.{u} Scalar (add (add a b) (add c d)) (add (add a c) (add b d))) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @eq_calc3.{u} Scalar (add (add a b) (add c d)) (add a (add b (add c d))) (add a (add c (add b d))) (add (add a c) (add b d)) (add_assoc_arg a b (add c d)) (@eq_congr_arg.{u,u} Scalar Scalar (fun (z : Scalar) => add a z) (add b (add c d)) (add c (add b d)) (@eq_calc3.{u} Scalar (add b (add c d)) (add (add b c) d) (add (add c b) d) (add c (add b d)) (@eq_symm.{u} Scalar (add (add b c) d) (add b (add c d)) (add_assoc_arg b c d)) (@eq_congr_arg.{u,u} Scalar Scalar (fun (z : Scalar) => add z d) (add b c) (add c b) (add_comm_arg b c)) (add_assoc_arg c b d))) (@eq_symm.{u} Scalar (add (add a c) (add b d)) (add a (add c (add b d))) (add_assoc_arg a c (add b d))))

theorem add_cross_and_sub_cross_cancel_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (a : Scalar), forall (b : Scalar), forall (x : Scalar), @Eq.{u} Scalar (add (add (add a x) b) (add (sub a x) b)) (add (add a a) (add b b)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun a => fun b => fun x => @eq_trans.{u} Scalar (add (add (add a x) b) (add (sub a x) b)) (add (add (add a x) (sub a x)) (add b b)) (add (add a a) (add b b)) (@add_pairwise_commute_from_ring_args.{u} Scalar zero one add neg sub mul ring_args (add a x) b (sub a x) b) (@eq_congr2.{u,u,u} Scalar Scalar Scalar add (add (add a x) (sub a x)) (add a a) (add b b) (add b b) (@eq_trans.{u} Scalar (add (add a x) (sub a x)) (add a (add x (sub a x))) (add a a) (ring_args (@Eq.{u} Scalar (add (add a x) (sub a x)) (add a (add x (sub a x)))) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => add_assoc_arg a x (sub a x))) (@eq_congr_arg.{u,u} Scalar Scalar (fun (z : Scalar) => add a z) (add x (sub a x)) a (@add_sub_cross_cancel_from_ring_args.{u} Scalar zero one add neg sub mul ring_args a x))) (@Eq.refl.{u} Scalar (add b b)))

theorem parallelogram_scalar_rhs_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (a : Scalar), forall (b : Scalar), forall (x : Scalar), @Eq.{u} Scalar (add (add (add a x) b) (add (sub a x) b)) (add (mul (@two.{u} Scalar one add) a) (mul (@two.{u} Scalar one add) b)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun a => fun b => fun x => @eq_calc3.{u} Scalar (add (add (add a x) b) (add (sub a x) b)) (add (add a a) (add b b)) (add (mul (@two.{u} Scalar one add) a) (add b b)) (add (mul (@two.{u} Scalar one add) a) (mul (@two.{u} Scalar one add) b)) (@add_cross_and_sub_cross_cancel_from_ring_args.{u} Scalar zero one add neg sub mul ring_args a b x) (@eq_congr2.{u,u,u} Scalar Scalar Scalar add (add a a) (mul (@two.{u} Scalar one add) a) (add b b) (add b b) (@eq_symm.{u} Scalar (mul (@two.{u} Scalar one add) a) (add a a) (@two_mul_from_ring_args.{u} Scalar zero one add neg sub mul ring_args a)) (@Eq.refl.{u} Scalar (add b b))) (@eq_congr2.{u,u,u} Scalar Scalar Scalar add (mul (@two.{u} Scalar one add) a) (mul (@two.{u} Scalar one add) a) (add b b) (mul (@two.{u} Scalar one add) b) (@Eq.refl.{u} Scalar (mul (@two.{u} Scalar one add) a)) (@eq_symm.{u} Scalar (mul (@two.{u} Scalar one add) b) (add b b) (@two_mul_from_ring_args.{u} Scalar zero one add neg sub mul ring_args b)))

theorem add_middle_to_front_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (a : Scalar), forall (x : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (add a x) b) (add x (add a b)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun a => fun x => fun b => ring_args (@Eq.{u} Scalar (add (add a x) b) (add x (add a b))) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @eq_calc3.{u} Scalar (add (add a x) b) (add a (add x b)) (add a (add b x)) (add x (add a b)) (add_assoc_arg a x b) (@eq_congr_arg.{u,u} Scalar Scalar (fun (z : Scalar) => add a z) (add x b) (add b x) (add_comm_arg x b)) (@eq_trans.{u} Scalar (add a (add b x)) (add (add a b) x) (add x (add a b)) (@eq_symm.{u} Scalar (add (add a b) x) (add a (add b x)) (add_assoc_arg a b x)) (add_comm_arg (add a b) x)))

theorem polarization_scalar_rhs_from_ring_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 (ring_args : @RingLawArgs.{u} Scalar zero one add neg sub mul), forall (nx : Scalar), forall (ny : Scalar), forall (d : Scalar), @Eq.{u} Scalar (mul (@two.{u} Scalar one add) d) (sub (add (add nx (mul (@two.{u} Scalar one add) d)) ny) (add nx ny)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun ring_args => fun nx => fun ny => fun d => ring_args (@Eq.{u} Scalar (mul (@two.{u} Scalar one add) d) (sub (add (add nx (mul (@two.{u} Scalar one add) d)) ny) (add nx ny))) (fun (sub_eq_add_neg_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub a b) (add a (neg b))) => fun (add_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add a b) c) (add a (add b c))) => fun (add_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add a b) (add b a)) => fun (add_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (add a zero) a) => fun (zero_add_arg : forall (a : Scalar), @Eq.{u} Scalar (add zero a) a) => fun (neg_add_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add (neg a) a) zero) => fun (add_neg_cancel_arg : forall (a : Scalar), @Eq.{u} Scalar (add a (neg a)) zero) => fun (sub_self_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a a) zero) => fun (mul_assoc_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (mul a b) c) (mul a (mul b c))) => fun (mul_comm_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (mul a b) (mul b a)) => fun (mul_one_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a one) a) => fun (one_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul one a) a) => fun (left_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul a (add b c)) (add (mul a b) (mul a c))) => fun (right_distrib_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (mul (add a b) c) (add (mul a c) (mul b c))) => fun (mul_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (mul a zero) zero) => fun (zero_mul_arg : forall (a : Scalar), @Eq.{u} Scalar (mul zero a) zero) => fun (add_left_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add a b) (add a c)), @Eq.{u} Scalar b c) => fun (ring_normalize_add_mul3_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (add (add (mul a b) (mul b c)) (mul a c)) (add (add (mul a b) (mul a c)) (mul b c))) => fun (add_right_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), forall (h : @Eq.{u} Scalar (add b a) (add c a)), @Eq.{u} Scalar b c) => fun (neg_neg_arg : forall (a : Scalar), @Eq.{u} Scalar (neg (neg a)) a) => fun (sub_zero_arg : forall (a : Scalar), @Eq.{u} Scalar (sub a zero) a) => fun (zero_sub_arg : forall (a : Scalar), @Eq.{u} Scalar (sub zero a) (neg a)) => fun (sub_add_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (add (sub a b) b) a) => fun (add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), @Eq.{u} Scalar (sub (add a b) b) a) => fun (sub_add_sub_cancel_arg : forall (a : Scalar), forall (b : Scalar), forall (c : Scalar), @Eq.{u} Scalar (sub (sub a c) (sub b c)) (sub a b)) => @eq_symm.{u} Scalar (sub (add (add nx (mul (@two.{u} Scalar one add) d)) ny) (add nx ny)) (mul (@two.{u} Scalar one add) d) (@eq_trans.{u} Scalar (sub (add (add nx (mul (@two.{u} Scalar one add) d)) ny) (add nx ny)) (sub (add (mul (@two.{u} Scalar one add) d) (add nx ny)) (add nx ny)) (mul (@two.{u} Scalar one add) d) (@eq_congr2.{u,u,u} Scalar Scalar Scalar sub (add (add nx (mul (@two.{u} Scalar one add) d)) ny) (add (mul (@two.{u} Scalar one add) d) (add nx ny)) (add nx ny) (add nx ny) (@add_middle_to_front_from_ring_args.{u} Scalar zero one add neg sub mul ring_args nx (mul (@two.{u} Scalar one add) d) ny) (@Eq.refl.{u} Scalar (add nx ny))) (add_sub_cancel_arg (mul (@two.{u} Scalar one add) d) (add nx ny))))