Graceful Tree Conjecture (Ringel–Kotzig conjecture)

lemma graceful_tree_one_vertex :
    let T : SimpleGraph Unit := ⊥
    let m := T.edgeFinset.card
    ∃ f : Unit → ℕ,
      Function.Injective f ∧
      (∀ v, f v ≤ m) ∧
      T.edgeFinset.image (fun e =>
        e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)),
                fun u v => by
                  show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbs
                  rw [← Int.natAbs_neg, neg_sub]⟩) = Finset.Icc 1 m := by
  sorry