theorem proved term proof

`exists_grayCover_of_le64`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 331theorem exists_grayCover_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
 332    ∃ w : GrayCover d (2 ^ d), w.path = brgcPath d :=

Term-mode proof.

 333  ⟨brgcGrayCover d hdpos hd, rfl⟩
 334
 335end GrayCycleGeneral
 336
 337end Patterns
 338end IndisputableMonolith

Lean names referenced from this declaration's body.