From 64a03e1677789967ce85324a53c531346d7c4a24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Bouchard?= <sebastien.bouchard@lip6.fr>
Date: Wed, 5 Jun 2024 19:11:20 +0200
Subject: [PATCH] Some proofs to help Even (to be copied in his branch)

---
 Util/ListComplements.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index 236ef412..ead544c0 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -52,6 +52,22 @@ intros x l Hin. induction l.
 - destruct Hin. subst. now left. right. auto.
 Qed. *)
 
+Lemma hd_proof : forall l : list A, 0 < length l -> A.
+Proof using .
+  intros * H. destruct l as [|a t]. 2: exact a. exfalso.
+  rewrite (proj2 (length_zero_iff_nil _)) in H by reflexivity.
+  inversion H.
+Qed.
+
+Lemma all_eq : forall (l : list A) (a1 : A), In a1 l ->length l = 1
+  -> forall a2 : A, In a2 l -> a2 = a1.
+Proof using .
+  intros * Hi1 H * Hi2. destruct l as [|h t].
+  rewrite (proj2 (length_zero_iff_nil _)) in H by reflexivity. discriminate H.
+  destruct t as [|h1 t]. cbn in Hi1, Hi2. destruct Hi1, Hi2. subst. reflexivity.
+  1-3: contradiction. exfalso. eapply Nat.neq_succ_0, eq_add_S, H.
+Qed.
+
 Lemma InA_Leibniz : forall (x : A) l, InA Logic.eq x l <-> In x l.
 Proof using .
 intros x l. split; intro Hl; induction l; inversion_clear Hl;
-- 
GitLab