1 files changed, 57 insertions, 0 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
new file mode 100644
index 00000000..9ba3fb2e
--- /dev/null
+++ b/test-suite/modules/PO.v
@@ -0,0 +1,57 @@
+Implicit Arguments On.
+
+Implicits fst.
+Implicits snd.
+
+Module Type PO.
+  Parameter T:Set.
+  Parameter le:T->T->Prop.
+  
+  Axiom le_refl : (x:T)(le x x).
+  Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z).
+  Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y).
+  
+  Hints Resolve le_refl le_trans le_antis.
+End PO.
+
+
+Module Pair[X:PO][Y:PO] <: PO.
+  Definition T:=X.T*Y.T.
+  Definition le:=[p1,p2]
+    (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
+
+  Hints Unfold le.
+
+  Lemma le_refl : (p:T)(le p p).
+    Info Auto.
+  Qed.
+
+  Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
+    Unfold le; Intuition; Info EAuto.
+  Qed.    
+
+  Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2).
+    NewDestruct p1.  
+    NewDestruct p2.
+    Unfold le.
+    Intuition.
+    CutRewrite t=t1.
+    CutRewrite t0=t2.
+    Reflexivity.
+
+    Info Auto.
+
+    Info Auto.
+  Qed.
+
+End Pair.
+
+
+
+Read Module Nat.
+
+Module NN := Pair Nat Nat.
+
+Lemma zz_min : (p:NN.T)(NN.le (O,O) p).
+  Info Auto with arith.
+Qed.