English
If for all i in Ioc m n one has r i (pred i) and m ≤ n, then there is a reflexive-transitive chain from n to m.
Русский
Если для всех i из Ioc(m,n) выполняется r(i, pred i) и m ≤ n, то существует рефлексивно-транзитивная цепочка от n к m.
LaTeX
$$\\forall i \\in \\mathrm{Ioc}(m,n),\\; r(i,\\mathrm{pred}\\, i) \\quad\\land\\quad m \\le n \\;\n\\Rightarrow\\; \\operatorname{ReflTransGen} r\, n\, m$$
Lean4
/-- For `m ≤ n`, `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ pred i`
for all `i` between `n` and `m`. -/
theorem reflTransGen_of_pred_of_ge (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc m n, r i (pred i)) (hnm : m ≤ n) :
ReflTransGen r n m :=
reflTransGen_of_succ_of_le (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hnm
