proposition: Lemma Acc_chains k x : (forall n y, chain n y x -> n <= k) -> Acc R x.
proof: Proof. revert x. induction k as [ | k IHk ]; intros x Hx. + constructor 1; intros y Hy. assert (chain 1 y x) as C. { constructor 2 with x. + trivial. + constructor 1. } apply Hx in C; lia. + constructor 1; intros y Hy. apply IHk; intros n z Hn. apply le_S_n. apply (Hx _ z). apply chain_snoc with y; auto. Qed.
imports: Arith List Lia