Format probe q3
ProvedTaoFivePrimes.zz_probe_q3probe
Probe: trivial identity with a single Definitions import. To be deprecated.
Preamble
import Mathlib import Definitions.Def_TaoFivePrimes_TypeIEnvelopeInterfaces
Formal statement
theorem TaoFivePrimes.zz_probe_q3 (n : ℕ) : n = n := by sorry