proposition: Fact chain_plus_inv a b x z : chain (a+b) x z -> exists y, chain a x y /\ chain b y z.
proof: Proof. revert x; induction a as [ | a IHa ]; intros x; simpl. + exists x; split; auto. + intros H. apply chain_inv_S in H. destruct H as (y & H1 & H2). specialize (IHa _ H2). destruct IHa as (k & ? & ?). exists k; split; auto. constructor 2 with y; auto. Qed.
imports: Arith List Lia