proposition: Fact chain_snoc_inv n x z : chain (S n) x z -> exists y, chain n x y /\ R y z.
proof: Proof. replace (S n) with (n+1) by lia. intros H; apply chain_plus_inv in H. destruct H as (y & H1 & H2). exists y; split; auto. apply chain_inv_S in H2. destruct H2 as (k & H2 & H3). apply chain_inv_0 in H3; subst; auto. Qed.
imports: Arith List Lia