[`SimpleGraph/Hamiltonian`] Graphs with Hamiltonian/Eulerian walks are connected

[SnirBroshi]

SimpleGraph.IsHamiltonian.connected exists for Hamiltonian graphs/cycles, but not for Hamiltonian walks.

import Mathlib
namespace SimpleGraph.Walk
variable {V : Type*} [DecidableEq V] {G : SimpleGraph V} {u v : V} {w : G.Walk u v}

theorem IsHamiltonian.connected (hw : w.IsHamiltonian) : G.Connected := by
  sorry

theorem IsEulerian.connected (hw : w.IsEulerian) (h : ∀ v, G.neighborSet v |>.Nonempty) :
    G.Connected := by
  sorry