Reachability of the unique sink in a finite ranked relation

theorem MagnitudeConjecture.RankedReachability.reaches_sink {V : Type u} [Fintype V] (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) (sink : V) (hsink : ∀ (x : V), (¬∃ (y : V), E x y) → x = sink) (x : V) : Relation.ReflTransGen E x sink

Reversing a bounded rank reduces sink reachability to source reachability.