let v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
a b c d : ℝ
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)