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