product_fst_pair_from_args

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)