Commit dfe225f7 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso

relations.nsteps: add inversion lemma for `nsteps R 1 a b`

parent 0b3d1e9f
......@@ -137,6 +137,8 @@ Section closure.
Lemma nsteps_once x y : R x y nsteps R 1 x y.
Proof. eauto. Qed.
Lemma nsteps_once_inv x y : nsteps R 1 x y R x y.
Proof. inversion 1 as [|???? Hhead Htail]; inversion Htail; by subst. Qed.
Lemma nsteps_trans n m x y z :
nsteps R n x y nsteps R m y z nsteps R (n + m) x z.
Proof. induction 1; simpl; eauto. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment