Mathlib.Analysis.NormedSpace.Basic

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.LinearAlgebra.VectorSpace

def NormDist.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (x : Vector), forall (y : Vector), Scalar :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun x => fun y => norm (@vsub.{v} Vector vadd vneg y x)

def NormedSpaceLawArgs.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => forall (P : Prop), forall (mk : forall (norm_nonneg_law : forall (x : Vector), le_rel zero (norm x)), forall (norm_zero_law : @Eq.{u} Scalar (norm vzero) zero), forall (norm_triangle_law : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))), forall (norm_neg_law : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)), forall (norm_dist_self_law : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero), forall (norm_dist_symm_law : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)), forall (norm_dist_triangle_law : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))), P), P

def ProductZero.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), Product :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => pair xzero yzero

def ProductAdd.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (left : Product), forall (right : Product), Product :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun left => fun right => pair (xadd (fst left) (fst right)) (yadd (snd left) (snd right))

def ProductNeg.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (point : Product), Product :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun point => pair (xneg (fst point)) (yneg (snd point))

def ProductSmul.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (a : Scalar), forall (point : Product), Product :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun a => fun point => pair (xsmul a (fst point)) (ysmul a (snd point))

def ProductSub.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (left : Product), forall (right : Product), Product :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun left => fun right => @ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right)

def ProductNorm.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (point : Product), Scalar :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun point => add (xnorm (fst point)) (ynorm (snd point))

def ProductDist.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (left : Product), forall (right : Product), Scalar :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun left => fun right => @ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductSub.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right left)

def ProductNormEstimateArgs.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => forall (P : Prop), forall (mk : forall (fst_pair_law : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x), forall (snd_pair_law : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y), forall (pair_eta_law : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point), forall (product_norm_fst_le_law : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)), forall (product_norm_snd_le_law : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)), forall (product_norm_pair_le_add_law : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)), forall (product_norm_add_le_law : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))), forall (product_dist_pair_le_add_law : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)), P), P

theorem norm_dist_def.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (norm (@vsub.{v} Vector vadd vneg y x)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun x => fun y => @Eq.refl.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y)

theorem norm_nonneg_from_args.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (norm_args : @NormedSpaceLawArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), forall (x : Vector), le_rel zero (norm x) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun norm_args => fun x => norm_args (le_rel zero (norm x)) (fun (norm_nonneg_arg : forall (x : Vector), le_rel zero (norm x)) => fun (norm_zero_arg : @Eq.{u} Scalar (norm vzero) zero) => fun (norm_triangle_arg : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))) => fun (norm_neg_arg : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)) => fun (norm_dist_self_arg : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) => fun (norm_dist_symm_arg : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) => fun (norm_dist_triangle_arg : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) => norm_nonneg_arg x)

theorem norm_zero_from_args.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (norm_args : @NormedSpaceLawArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), @Eq.{u} Scalar (norm vzero) zero :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun norm_args => norm_args (@Eq.{u} Scalar (norm vzero) zero) (fun (norm_nonneg_arg : forall (x : Vector), le_rel zero (norm x)) => fun (norm_zero_arg : @Eq.{u} Scalar (norm vzero) zero) => fun (norm_triangle_arg : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))) => fun (norm_neg_arg : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)) => fun (norm_dist_self_arg : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) => fun (norm_dist_symm_arg : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) => fun (norm_dist_triangle_arg : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) => norm_zero_arg)

theorem norm_triangle_from_args.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (norm_args : @NormedSpaceLawArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun norm_args => fun x => fun y => norm_args (le_rel (norm (vadd x y)) (add (norm x) (norm y))) (fun (norm_nonneg_arg : forall (x : Vector), le_rel zero (norm x)) => fun (norm_zero_arg : @Eq.{u} Scalar (norm vzero) zero) => fun (norm_triangle_arg : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))) => fun (norm_neg_arg : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)) => fun (norm_dist_self_arg : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) => fun (norm_dist_symm_arg : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) => fun (norm_dist_triangle_arg : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) => norm_triangle_arg x y)

theorem norm_neg_from_args.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (norm_args : @NormedSpaceLawArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun norm_args => fun x => norm_args (@Eq.{u} Scalar (norm (vneg x)) (norm x)) (fun (norm_nonneg_arg : forall (x : Vector), le_rel zero (norm x)) => fun (norm_zero_arg : @Eq.{u} Scalar (norm vzero) zero) => fun (norm_triangle_arg : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))) => fun (norm_neg_arg : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)) => fun (norm_dist_self_arg : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) => fun (norm_dist_symm_arg : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) => fun (norm_dist_triangle_arg : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) => norm_neg_arg x)

theorem norm_dist_self_from_args.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (norm_args : @NormedSpaceLawArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun norm_args => fun x => norm_args (@Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) (fun (norm_nonneg_arg : forall (x : Vector), le_rel zero (norm x)) => fun (norm_zero_arg : @Eq.{u} Scalar (norm vzero) zero) => fun (norm_triangle_arg : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))) => fun (norm_neg_arg : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)) => fun (norm_dist_self_arg : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) => fun (norm_dist_symm_arg : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) => fun (norm_dist_triangle_arg : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) => norm_dist_self_arg x)

theorem norm_dist_symm_from_args.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (norm_args : @NormedSpaceLawArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun norm_args => fun x => fun y => norm_args (@Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) (fun (norm_nonneg_arg : forall (x : Vector), le_rel zero (norm x)) => fun (norm_zero_arg : @Eq.{u} Scalar (norm vzero) zero) => fun (norm_triangle_arg : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))) => fun (norm_neg_arg : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)) => fun (norm_dist_self_arg : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) => fun (norm_dist_symm_arg : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) => fun (norm_dist_triangle_arg : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) => norm_dist_symm_arg x y)

theorem norm_dist_triangle_from_args.{u,v} :
  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 (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (norm_args : @NormedSpaceLawArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun norm_args => fun x => fun y => fun z => norm_args (le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) (fun (norm_nonneg_arg : forall (x : Vector), le_rel zero (norm x)) => fun (norm_zero_arg : @Eq.{u} Scalar (norm vzero) zero) => fun (norm_triangle_arg : forall (x : Vector), forall (y : Vector), le_rel (norm (vadd x y)) (add (norm x) (norm y))) => fun (norm_neg_arg : forall (x : Vector), @Eq.{u} Scalar (norm (vneg x)) (norm x)) => fun (norm_dist_self_arg : forall (x : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x x) zero) => fun (norm_dist_symm_arg : forall (x : Vector), forall (y : Vector), @Eq.{u} Scalar (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y x)) => fun (norm_dist_triangle_arg : forall (x : Vector), forall (y : Vector), forall (z : Vector), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x z) (add (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y) (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm y z))) => norm_dist_triangle_arg x y z)

theorem product_zero_def.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), @Eq.{p} Product (@ProductZero.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (pair xzero yzero) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => @Eq.refl.{p} Product (@ProductZero.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd)

theorem product_add_def.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (left : Product), forall (right : Product), @Eq.{p} Product (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right) (pair (xadd (fst left) (fst right)) (yadd (snd left) (snd right))) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun left => fun right => @Eq.refl.{p} Product (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)

theorem product_neg_def.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (point : Product), @Eq.{p} Product (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point) (pair (xneg (fst point)) (yneg (snd point))) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun point => @Eq.refl.{p} Product (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)

theorem product_smul_def.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (a : Scalar), forall (point : Product), @Eq.{p} Product (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd a point) (pair (xsmul a (fst point)) (ysmul a (snd point))) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun a => fun point => @Eq.refl.{p} Product (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd a point)

theorem product_sub_def.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (left : Product), forall (right : Product), @Eq.{p} Product (@ProductSub.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right) (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun left => fun right => @Eq.refl.{p} Product (@ProductSub.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)

theorem product_norm_def.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (point : Product), @Eq.{u} Scalar (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point) (add (xnorm (fst point)) (ynorm (snd point))) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun point => @Eq.refl.{u} Scalar (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)

theorem product_dist_def.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (left : Product), forall (right : Product), @Eq.{u} Scalar (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductSub.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right left)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun left => fun right => @Eq.refl.{u} Scalar (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)

theorem product_fst_pair_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun x => fun y => product_args (@Eq.{v} X (fst (pair x y)) x) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => fst_pair_arg x y)

theorem product_snd_pair_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun x => fun y => product_args (@Eq.{w} Y (snd (pair x y)) y) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => snd_pair_arg x y)

theorem product_pair_eta_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun point => product_args (@Eq.{p} Product (pair (fst point) (snd point)) point) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => pair_eta_arg point)

theorem product_add_fst_from_pair_law.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (fst_pair_law : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x), forall (left : Product), forall (right : Product), @Eq.{v} X (fst (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (xadd (fst left) (fst right)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun fst_pair_law => fun left => fun right => fst_pair_law (xadd (fst left) (fst right)) (yadd (snd left) (snd right))

theorem product_add_snd_from_pair_law.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (snd_pair_law : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y), forall (left : Product), forall (right : Product), @Eq.{w} Y (snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (yadd (snd left) (snd right)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun snd_pair_law => fun left => fun right => snd_pair_law (xadd (fst left) (fst right)) (yadd (snd left) (snd right))

theorem product_smul_fst_from_pair_law.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (fst_pair_law : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x), forall (a : Scalar), forall (point : Product), @Eq.{v} X (fst (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd a point)) (xsmul a (fst point)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun fst_pair_law => fun a => fun point => fst_pair_law (xsmul a (fst point)) (ysmul a (snd point))

theorem product_smul_snd_from_pair_law.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (snd_pair_law : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y), forall (a : Scalar), forall (point : Product), @Eq.{w} Y (snd (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd a point)) (ysmul a (snd point)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun snd_pair_law => fun a => fun point => snd_pair_law (xsmul a (fst point)) (ysmul a (snd point))

theorem product_norm_pair_eq_from_pair_laws.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (fst_pair_law : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x), forall (snd_pair_law : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y), forall (x : X), forall (y : Y), @Eq.{u} Scalar (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add (xnorm x) (ynorm y)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun fst_pair_law => fun snd_pair_law => fun x => fun y => @eq_congr2.{u,u,u} Scalar Scalar Scalar add (xnorm (fst (pair x y))) (xnorm x) (ynorm (snd (pair x y))) (ynorm y) (@eq_congr_arg.{v,u} X Scalar xnorm (fst (pair x y)) x (fst_pair_law x y)) (@eq_congr_arg.{w,u} Y Scalar ynorm (snd (pair x y)) y (snd_pair_law x y))

theorem product_norm_fst_le_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun point => product_args (le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => product_norm_fst_le_arg point)

theorem product_norm_snd_le_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun point => product_args (le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => product_norm_snd_le_arg point)

theorem product_norm_pair_le_add_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun x => fun y => fun bx => fun bound_y => fun hx => fun hy => product_args (le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => product_norm_pair_le_add_arg x y bx bound_y hx hy)

theorem product_norm_add_le_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun left => fun right => product_args (le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => product_norm_add_le_arg left right)

theorem product_dist_pair_le_add_from_args.{p,u,v,w} :
  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 (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (product_args : @ProductNormEstimateArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun product_args => fun x1 => fun x2 => fun y1 => fun y2 => fun bx => fun bound_y => fun hx => fun hy => product_args (le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) (fun (fst_pair_arg : forall (x : X), forall (y : Y), @Eq.{v} X (fst (pair x y)) x) => fun (snd_pair_arg : forall (x : X), forall (y : Y), @Eq.{w} Y (snd (pair x y)) y) => fun (pair_eta_arg : forall (point : Product), @Eq.{p} Product (pair (fst point) (snd point)) point) => fun (product_norm_fst_le_arg : forall (point : Product), le_rel (xnorm (fst point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_snd_le_arg : forall (point : Product), le_rel (ynorm (snd point)) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd point)) => fun (product_norm_pair_le_add_arg : forall (x : X), forall (y : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm x) bx), forall (hy : le_rel (ynorm y) bound_y), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x y)) (add bx bound_y)) => fun (product_norm_add_le_arg : forall (left : Product), forall (right : Product), le_rel (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left right)) (add (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd left) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd right))) => fun (product_dist_pair_le_add_arg : forall (x1 : X), forall (x2 : X), forall (y1 : Y), forall (y2 : Y), forall (bx : Scalar), forall (bound_y : Scalar), forall (hx : le_rel (xnorm (@vsub.{v} X xadd xneg x2 x1)) bx), forall (hy : le_rel (ynorm (@vsub.{w} Y yadd yneg y2 y1)) bound_y), le_rel (@ProductDist.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd (pair x1 y1) (pair x2 y2)) (add bx bound_y)) => product_dist_pair_le_add_arg x1 x2 y1 y2 bx bound_y hx hy)