proposition: Lemma tc_nsteps x y : tc R x y ↔ ∃ n, 0 < n ∧ nsteps R n x y.
proof: Proof. split. - induction 1 as [|x1 x2 y ?? (n&?&?)]. { exists 1. eauto using nsteps_once with lia. } exists (S n); eauto using nsteps_l. - intros (n & ? & Hstep). induction Hstep as [|n x1 x2 y ? Hstep]; [lia|]. destruct Hstep; eauto with lia. Qed.
imports: stdpp(options)