From 8843bce00acc288e4e51ab6d8072257c79a3cb95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 18 Feb 2026 13:44:03 +0100
Subject: [PATCH] Wellfounded/Inclusion.v add lemma for when the inclusion is
 partial

---
 theories/Wellfounded/Inclusion.v | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index e565dde47d..c200585408 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -10,16 +10,32 @@
 
 (** Author: Bruno Barras *)
 
-From Stdlib Require Import Relation_Definitions.
+From Stdlib Require Import Relation_Definitions Relation_Operators.
 
 Section WfInclusion.
   Variable A : Type.
   Variables R1 R2 : A -> A -> Prop.
 
+  Lemma Acc_partial_incl : forall z : A,
+      (forall x y, clos_refl_trans _ R1 y z -> R1 x y -> R2 x y) ->
+      Acc R2 z -> Acc R1 z.
+  Proof.
+    intros z H.
+    induction 1 as [z Hz IH].
+    apply Acc_intro.
+    intros y Hy.
+    apply IH.
+    - apply H,Hy.
+      auto with sets.
+    - intros x z' Hz' HR.
+      apply H, HR.
+      apply rt_trans with y;auto with sets.
+  Qed.
+
   Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
   Proof.
     induction 2.
-    apply Acc_intro; auto with sets.
+    apply Acc_intro; auto.
   Qed.
 
   #[local]
@@ -27,7 +43,7 @@ Section WfInclusion.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
   Proof.
-    unfold well_founded; auto with sets.
+    unfold well_founded; auto.
   Qed.
 
 End WfInclusion.