theorem proved term proof

`exists_grayCycle_of_le64`

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

formal statement (Lean)

 327theorem exists_grayCycle_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
 328    ∃ w : GrayCycle d, w.path = brgcPath d :=

Term-mode proof.

 329  ⟨brgcGrayCycle d hdpos hd, rfl⟩
 330

Lean names referenced from this declaration's body.