proposition: Lemma rtc_intro_seq A (R : rel A) f i : forall j, i <= j -> (forall k, i <= k < j -> R (f k) (f (1+k))) -> R# (f i) (f j).
proof: Proof. cut (forall n, (forall k, i <= k < i + n -> R (f k) (f (1+k))) -> R# (f i) (f (n+i))). intros h j ij hij. assert (j = (j-i) + i). lia. rewrite H. apply h. intros k hk. apply hij. lia. induction n; intro h. refl. trans (f (n+i)). apply IHn. intros k hk. apply h. lia. apply rt_step. apply h. lia. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)