2 files changed, 54 insertions, 0 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index ef292d4c1..e87f436ed 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -164,3 +164,37 @@ Qed.
 
 Hints Resolve lt_wf : arith.
 Hints Resolve well_founded_lt_compat : arith.
+
+Section LT_WF_REL.
+Variable A :Set.
+Variable R:A->A->Prop.
+
+(* Relational form of inversion *)
+Variable F : A -> nat -> Prop.
+Definition inv_lt_rel 
+ [x,y]:=(EX n | (F x n) & (m:nat)(F y m)->(lt n m)).
+
+Hypothesis F_compat : (x,y:A) (R x y) -> (inv_lt_rel x y).
+Remark acc_lt_rel : 
+  (x:A)(EX n | (F x n))->(Acc A R x).
+Intros x (n,fxn); Generalize x fxn; Clear x fxn.
+Pattern n; Apply lt_wf_ind; Intros.
+Constructor; Intros.
+Case (F_compat y x); Trivial; Intros.
+Apply (H x0); Auto.
+Save.
+
+Theorem well_founded_inv_lt_rel_compat : (well_founded A R).
+Constructor; Intros.
+Case (F_compat y a); Trivial; Intros.
+Apply acc_lt_rel; Trivial.
+Exists x; Trivial.
+Save.
+
+
+End LT_WF_REL.
+
+Lemma well_founded_inv_rel_inv_lt_rel 
+  : (A:Set)(F:A->nat->Prop)(well_founded A (inv_lt_rel A F)).
+Intros; Apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); Trivial.
+Save.
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index f29151cae..9afffc95c 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -33,6 +33,26 @@ Section Inverse_Image.
     Red; Intros; Apply Acc_inverse_image; Auto.
   Qed.
 
+  Variable F : A -> B -> Prop.
+  Local RoF : A -> A -> Prop := [x,y]
+    (EX b : B | (F x b) & (c:B)(F y c)->(R b c)).
+
+Lemma Acc_inverse_rel :
+   (b:B)(Acc B R b)->(x:A)(F x b)->(Acc A RoF x).
+Induction 1; Intros.
+Constructor; Intros.
+Case H3; Intros.
+Apply (H1 x1); Auto.
+Save.
+
+
+Theorem wf_inverse_rel : 
+   (well_founded B R)->(well_founded A RoF).
+    Red; Constructor; Intros.
+    Case H0; Intros.
+    Apply (Acc_inverse_rel x); Auto.
+Save.
+
 End Inverse_Image.