Si ab = cd y e = f, entonces a(be) = c(df)
Demostrar con Lean4 que si ab = cd y e = f, entonces a(be) = c(df)
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c d e f : ℝ) (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := by sorry |