proposition: Corollary chain_snoc n x y z : chain n x y -> R y z -> chain (S n) x z.
proof: Proof. intros H1 H2. replace (S n) with (n+1) by lia. apply chain_plus with y; auto. constructor 2 with z; auto. Qed.
imports: Arith List Lia