ajout inverse relation bien fondee

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4000 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

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.