From dfe225f71c86ab346bfc8681f04ef9c9431ae0f8 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 21 Aug 2019 16:39:53 +0200
Subject: [PATCH] relations.nsteps: add inversion lemma for `nsteps R 1 a b`

---
 theories/relations.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/relations.v b/theories/relations.v
index 8b8a3696..2684b647 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -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.
-- 
GitLab