Collatz reachability

Conjectura.Defs.Mathematics.NumberTheory.CollatzReaches

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Defs.Mathematics.NumberTheory.CollatzStep
import Mathlib.Logic.Relation

/-! # Collatz reachability -/

namespace Conjectura.NumberTheory

/-- `CollatzReaches m n` holds when iterating `collatzStep` from `m` eventually gives `n`. -/
def CollatzReaches (m n : ℕ) : Prop :=
  Relation.ReflTransGen (fun a b => b = collatzStep a) m n

end Conjectura.NumberTheory