proposition: Fact chain_chain_list n x y : chain n x y -> exists l, chain_list l x y /\ n = length l.
proof: Proof. induction 1 as [ x | n x y z H1 _ (l & H2 & H3) ]; auto. + exists nil; simpl; split; auto; constructor. + exists (x::l); simpl; split; auto; constructor 2 with y; auto. Qed.
imports: Arith List Lia