From 82bc79b24542202f4e4ded147a81c071a57daadb Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Wed, 6 Dec 2023 08:21:51 +0100
Subject: [PATCH] Update

---
 src/subsequences2.v | 29 ++++++++++++-----------------
 1 file changed, 12 insertions(+), 17 deletions(-)

diff --git a/src/subsequences2.v b/src/subsequences2.v
index 28a41aa..15d8cda 100644
--- a/src/subsequences2.v
+++ b/src/subsequences2.v
@@ -223,21 +223,12 @@ Proof.
 Qed.
 
 
-
-
-
-
-
-
-
-
-Theorem subsequence_trans {X: Type} :
+Theorem Subsequence_trans {X: Type} :
   forall (l1 l2 l3: list X),
-  subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.
+  Subsequence l1 l2 -> Subsequence l2 l3 -> Subsequence l1 l3.
 Proof.
-  intros l1 l2 l3. intros H I.
-  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
-  apply subsequence_eq_def_1 in I.
+  intros l1 l2 l3. intros H I. apply Subsequence_bools.
+  apply Subsequence_flat_map in H. apply Subsequence_bools in I.
   destruct H. destruct H. destruct H. destruct I. destruct H1.
   exists (
     (repeat false (length x)) ++
@@ -301,12 +292,11 @@ Proof.
 Qed.
 
 
-Lemma subsequence_length {X: Type} :
-  forall (u v: list X), subsequence u v -> length v <= length u.
+Theorem Subsequence_length {X: Type} :
+  forall (u v: list X), Subsequence u v -> length v <= length u.
 Proof.
   intros u v. generalize u. induction v; intro u0; intro H. apply Nat.le_0_l.
-  apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
-  destruct H. destruct H. destruct H. apply subsequence_eq_def_3 in H0.
+  destruct H. destruct H. destruct H.
   apply IHv in H0. simpl. apply Nat.le_succ_l. rewrite H.
   rewrite app_length. apply Nat.lt_lt_add_l.
   rewrite <- Nat.le_succ_l. simpl. rewrite <- Nat.succ_le_mono.
@@ -314,6 +304,11 @@ Proof.
 Qed.
 
 
+
+
+
+
+
 Theorem subsequence_eq {X: Type} :
   forall (u v: list X),
   subsequence u v -> subsequence v u -> u = v.