Si c = ba-d y d = ab, entonces c = 0
Demostrar con Lean4 que si a, b, c y d son números reales tales
1 2 |
c = b * a - d d = a * b |
entonces
1 |
c = 0 |
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by sorry |