Bibliotheque Num

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

19 files changed, 394 insertions, 19 deletions

diff --git a/theories/Num/.depend b/theories/Num/.depend
new file mode 100644
index 000000000..24658d7ca
--- /dev/null
+++ b/theories/Num/.depend
@@ -0,0 +1,66 @@
+SubProps.vo: SubProps.v
+SubProps.vi: SubProps.v
+Params.vo: Params.v
+Params.vi: Params.v
+OppProps.vo: OppProps.v
+OppProps.vi: OppProps.v
+OppAxioms.vo: OppAxioms.v
+OppAxioms.vi: OppAxioms.v
+NeqDef.vo: NeqDef.v Params.vo EqParams.vo
+NeqDef.vi: NeqDef.v Params.vo EqParams.vo
+NatSyntax.vo: NatSyntax.v
+NatSyntax.vi: NatSyntax.v
+NSyntax.vo: NSyntax.v Params.vo EqParams.vo NeqDef.vo
+NSyntax.vi: NSyntax.v Params.vo EqParams.vo NeqDef.vo
+LtProps.vo: LtProps.v Axioms.vo AddProps.vo
+LtProps.vi: LtProps.v Axioms.vo AddProps.vo
+LeibnizEq.vo: LeibnizEq.v Params.vo
+LeibnizEq.vi: LeibnizEq.v Params.vo
+LeProps.vo: LeProps.v LtProps.vo LeAxioms.vo
+LeProps.vi: LeProps.v LtProps.vo LeAxioms.vo
+LeAxioms.vo: LeAxioms.v Axioms.vo LtProps.vo
+LeAxioms.vi: LeAxioms.v Axioms.vo LtProps.vo
+GtProps.vo: GtProps.v
+GtProps.vi: GtProps.v
+GtAxioms.vo: GtAxioms.v Axioms.vo LeProps.vo
+GtAxioms.vi: GtAxioms.v Axioms.vo LeProps.vo
+GeProps.vo: GeProps.v
+GeProps.vi: GeProps.v
+GeAxioms.vo: GeAxioms.v Axioms.vo LtProps.vo
+GeAxioms.vi: GeAxioms.v Axioms.vo LtProps.vo
+EqParams.vo: EqParams.v Params.vo
+EqParams.vi: EqParams.v Params.vo
+EqAxioms.vo: EqAxioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
+EqAxioms.vi: EqAxioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
+DiscrProps.vo: DiscrProps.v DiscrAxioms.vo LtProps.vo
+DiscrProps.vi: DiscrProps.v DiscrAxioms.vo LtProps.vo
+DiscrAxioms.vo: DiscrAxioms.v Params.vo NSyntax.vo
+DiscrAxioms.vi: DiscrAxioms.v Params.vo NSyntax.vo
+Definitions.vo: Definitions.v
+Definitions.vi: Definitions.v
+Axioms.vo: Axioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
+Axioms.vi: Axioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
+AddProps.vo: AddProps.v Axioms.vo
+AddProps.vi: AddProps.v Axioms.vo
+SubProps.html: SubProps.v
+Params.html: Params.v
+OppProps.html: OppProps.v
+OppAxioms.html: OppAxioms.v
+NeqDef.html: NeqDef.v Params.html EqParams.html
+NatSyntax.html: NatSyntax.v
+NSyntax.html: NSyntax.v Params.html EqParams.html NeqDef.html
+LtProps.html: LtProps.v Axioms.html AddProps.html
+LeibnizEq.html: LeibnizEq.v Params.html
+LeProps.html: LeProps.v LtProps.html LeAxioms.html
+LeAxioms.html: LeAxioms.v Axioms.html LtProps.html
+GtProps.html: GtProps.v
+GtAxioms.html: GtAxioms.v Axioms.html LeProps.html
+GeProps.html: GeProps.v
+GeAxioms.html: GeAxioms.v Axioms.html LtProps.html
+EqParams.html: EqParams.v Params.html
+EqAxioms.html: EqAxioms.v Params.html EqParams.html NeqDef.html NSyntax.html
+DiscrProps.html: DiscrProps.v DiscrAxioms.html LtProps.html
+DiscrAxioms.html: DiscrAxioms.v Params.html NSyntax.html
+Definitions.html: Definitions.v
+Axioms.html: Axioms.v Params.html EqParams.html NeqDef.html NSyntax.html
+AddProps.html: AddProps.v Axioms.html
diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
index cc48a8744..563392146 100644
--- a/theories/Num/AddProps.v
+++ b/theories/Num/AddProps.v
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 Require Export Axioms.
+Require Export EqAxioms.
 
 (*s This file contains basic properties of addition with respect to equality *)
 
diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v
index c9ada6ebc..804dc479c 100644
--- a/theories/Num/Axioms.v
+++ b/theories/Num/Axioms.v
@@ -9,6 +9,7 @@
 
 (*s Axioms for the basic numerical operations *)
 Require Export Params.
+Require Export EqParams.
 Require Export NeqDef.
 Require Export NSyntax.
 
@@ -21,12 +22,10 @@ Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
 (*s Axioms for [add] *)
 
 Axiom add_sym : (x,y:N)(x+y)=(y+x).
-Axiom add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
 Axiom add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)).
 Axiom add_0_x : (x:N)(zero+x)=x.
 
 (*s Axioms for [S] *)
-Axiom S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
 Axiom add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)).
 
 (*s Axioms for [one] *)
@@ -41,11 +40,7 @@ Axiom lt_anti_refl : (x:N)~(x<x).
 Axiom lt_x_Sx : (x:N)x<(S x).
 Axiom lt_S_compat : (x,y:N)(x<y)->(S x)<(S y).
 
-Axiom lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
 Axiom lt_add_compat_l : (x,y,z:N)(x<y)->((x+z)<(y+z)).
 
-Hints Resolve eq_refl eq_trans add_sym add_eq_compat add_assoc_l add_0_x 
-	      S_eq_compat add_Sx_y S_0_1 lt_x_Sx lt_S_compat
-              lt_trans lt_anti_refl lt_eq_compat lt_add_compat_l : num.
-Hints Immediate eq_sym : num.
-  
\ No newline at end of file
+Hints Resolve add_sym add_assoc_l add_0_x add_Sx_y S_0_1 lt_x_Sx lt_S_compat
+              lt_trans lt_anti_refl lt_add_compat_l : num.
diff --git a/theories/Num/EqAxioms.v b/theories/Num/EqAxioms.v
new file mode 100644
index 000000000..1741c3d1f
--- /dev/null
+++ b/theories/Num/EqAxioms.v
@@ -0,0 +1,25 @@
+(*i $Id: i*)
+
+(*s Axioms for equality *)
+Require Export Params.
+Require Export EqParams.
+Require Export NeqDef.
+Require Export NSyntax.
+
+(*s Basic Axioms for [eq] *)
+
+Axiom eq_refl : (x:N)(x=x).
+Axiom eq_sym : (x,y:N)(x=y)->(y=x).
+Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
+
+(*s Axioms for [eq] and [add] *)
+Axiom add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
+
+(*s Axioms for [eq] and [S] *)
+Axiom S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
+
+(*s Axioms for [eq] and [<] *)
+Axiom lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
+
+Hints Resolve eq_refl eq_trans add_eq_compat S_eq_compat lt_eq_compat : num.
+Hints Immediate eq_sym : num.
diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v
new file mode 100644
index 000000000..441dc21df
--- /dev/null
+++ b/theories/Num/EqParams.v
@@ -0,0 +1,17 @@
+(*i $Id $ i*)
+
+(*s Equality is introduced as an independant parameter, it could be 
+    instantiated with Leibniz equality *)
+Require Params.
+
+Parameter eqN:N->N->Prop.  
+
+(*i Infix 6 "=" eq. i*)
+
+Grammar constr constr1 :=
+eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
+
+Syntax constr
+  level 1:
+    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+.
\ No newline at end of file
diff --git a/theories/Num/Leibniz/.depend b/theories/Num/Leibniz/.depend
new file mode 100644
index 000000000..b6ddc78aa
--- /dev/null
+++ b/theories/Num/Leibniz/.depend
@@ -0,0 +1,9 @@
+Params.vo: Params.v
+Params.vi: Params.v
+NSyntax.vo: NSyntax.v Params.vo
+NSyntax.vi: NSyntax.v Params.vo
+EqAxioms.vo: EqAxioms.v NSyntax.vo
+EqAxioms.vi: EqAxioms.v NSyntax.vo
+Params.html: Params.v
+NSyntax.html: NSyntax.v Params.html
+EqAxioms.html: EqAxioms.v NSyntax.html
diff --git a/theories/Num/Leibniz/EqAxioms.v b/theories/Num/Leibniz/EqAxioms.v
new file mode 100644
index 000000000..46d835eeb
--- /dev/null
+++ b/theories/Num/Leibniz/EqAxioms.v
@@ -0,0 +1,50 @@
+
+(*s Instantiating [eqN] with Leibniz equality *)
+
+Require NSyntax.
+
+Definition eqN [x,y:N] := (x==y).
+Hints Unfold eqN : num.
+
+Grammar constr constr1 :=
+eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
+
+Syntax constr
+  level 1:
+    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ].
+
+(*s Lemmas for [eqN] *)
+
+Lemma eq_refl : (x:N)(x=x).
+Auto with num.
+Save.
+
+Lemma eq_sym : (x,y:N)(x=y)->(y=x).
+Unfold eqN; Auto.
+Save.
+
+Lemma eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
+Intros; Red; Transitivity y; Auto.
+Save.
+
+Hints Resolve eq_refl eq_trans : num.
+Hints Immediate eq_sym : num.
+
+(*s Compatibility lemmas for [S], [add], [lt] *)
+Lemma S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
+Intros x y eq1; Unfold eqN; Rewrite eq1; Auto.
+Save.
+Hints Resolve S_eq_compat : nat.
+
+Lemma add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
+Intros x1 x2 y1 y2 eq1 eq2;Unfold eqN;  Rewrite eq1; Rewrite eq2; Auto.
+Save.
+Hints Resolve add_eq_compat : nat.
+
+Lemma lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
+Intros x1 x2 y1 y2 eq1 eq2; Unfold eqN; Rewrite eq1; Rewrite eq2; Trivial.
+Save.
+
+Hints Resolve add_eq_compat S_eq_compat lt_eq_compat : num.
+
+ 
\ No newline at end of file
diff --git a/theories/Num/Leibniz/Make b/theories/Num/Leibniz/Make
new file mode 100644
index 000000000..0b35afabb
--- /dev/null
+++ b/theories/Num/Leibniz/Make
@@ -0,0 +1,3 @@
+EqAxioms.v 
+NSyntax.v 
+Params.v 
diff --git a/theories/Num/Leibniz/NSyntax.v b/theories/Num/Leibniz/NSyntax.v
new file mode 100644
index 000000000..62613512b
--- /dev/null
+++ b/theories/Num/Leibniz/NSyntax.v
@@ -0,0 +1,32 @@
+
+(*s Syntax for arithmetic *)
+
+Require Export Params.
+
+Infix 6 "<" lt.
+Infix 6 "<=" le.
+Infix 6 ">" gt.
+Infix 6 ">=" ge.
+
+(*i Infix 7 "+" plus. i*)
+
+Grammar constr lassoc_constr4 :=
+  squash_sum
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
+      case [$c2] of
+        (SQUASH $T2) ->
+            case [$c1] of
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
+            esac
+      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
+      esac.
+
+Syntax constr
+  level 1:
+    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+ ;
+
+  level 4:
+    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
+.
\ No newline at end of file
diff --git a/theories/Num/Leibniz/Params.v b/theories/Num/Leibniz/Params.v
new file mode 100644
index 000000000..a7be171b8
--- /dev/null
+++ b/theories/Num/Leibniz/Params.v
@@ -0,0 +1,20 @@
+(*i $Id $ i*)
+
+(*s 
+  Axiomatisation of a numerical set 
+  It will be instantiated by Z and R later on
+  We choose to introduce many operation to allow flexibility in definition 
+  ([S] is primitive in the definition of [nat] while [add] and [one] 
+   are primitive in the definition 
+*)
+
+Parameter N:Type.
+Parameter zero:N.
+Parameter one:N.
+Parameter add:N->N->N.
+Parameter S:N->N.
+
+(*s Relations, equality is defined separately *)
+Parameter lt,le,gt,ge:N->N->Prop.    
+
+
diff --git a/theories/Num/Make b/theories/Num/Make
index d01e6943e..d897d8087 100644
--- a/theories/Num/Make
+++ b/theories/Num/Make
@@ -1,7 +1,9 @@
 Params.v
+EqParams.v
 NeqDef.v
 NSyntax.v
 Axioms.v
+EqAxioms.v
 AddProps.v
 LtProps.v
 OppProps.v
@@ -15,6 +17,5 @@ GeProps.v
 DiscrAxioms.v
 DiscrProps.v
 OppAxioms.v
-NatParams.v
-NatSyntax.v
-NatAxioms.v
\ No newline at end of file
+Leibniz
+Nat
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index 488f900e5..443056fd8 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -9,18 +9,11 @@
 (*s Syntax for arithmetic *)
 
 Require Export Params.
-Require Export NeqDef.
 
 Infix 6 "<" lt.
 Infix 6 "<=" le.
 Infix 6 ">" gt.
 Infix 6 ">=" ge.
-Infix 6 "<>" neq.
-
-(*i Infix 6 "=" eq. i*)
-
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq $c $c2) ].
 
 (*i Infix 7 "+" plus. i*)
 
@@ -38,7 +31,7 @@ Grammar constr lassoc_constr4 :=
 
 Syntax constr
   level 1:
-    equal [ (eq $t1  $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
  ;
 
   level 4:
diff --git a/theories/Num/Nat/.depend b/theories/Num/Nat/.depend
new file mode 100644
index 000000000..8e81ee7c9
--- /dev/null
+++ b/theories/Num/Nat/.depend
@@ -0,0 +1,15 @@
+Params.vo: Params.v
+Params.vi: Params.v
+NeqDef.vo: NeqDef.v Params.vo
+NeqDef.vi: NeqDef.v Params.vo
+NSyntax.vo: NSyntax.v
+NSyntax.vi: NSyntax.v
+EqAxioms.vo: EqAxioms.v NSyntax.vo
+EqAxioms.vi: EqAxioms.v NSyntax.vo
+Axioms.vo: Axioms.v Params.vo NSyntax.vo
+Axioms.vi: Axioms.v Params.vo NSyntax.vo
+Params.html: Params.v
+NeqDef.html: NeqDef.v Params.html
+NSyntax.html: NSyntax.v
+EqAxioms.html: EqAxioms.v NSyntax.html
+Axioms.html: Axioms.v Params.html NSyntax.html
diff --git a/theories/Num/Nat/Axioms.v b/theories/Num/Nat/Axioms.v
new file mode 100644
index 000000000..3210cbd71
--- /dev/null
+++ b/theories/Num/Nat/Axioms.v
@@ -0,0 +1,83 @@
+(*i $Id: i*)
+
+(*s Axioms for the basic numerical operations *)
+Require Export Params.
+Require Export EqAxioms.
+Require NSyntax.
+
+(*s Lemmas for [add] *)
+
+Lemma add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)).
+Induction y; Simpl; Auto with nat.
+Save.
+Hints Resolve add_Sx_y : nat.
+
+(*s Lemmas for [add] *)
+
+Lemma add_0_x : (x:N)(zero+x)=x.
+Induction x; Simpl; Auto with nat.
+Save.
+Hints Resolve add_0_x : nat.
+
+Lemma add_sym : (x,y:N)(x+y)=(y+x).
+Intros x y; Elim y; Simpl; Intros; Auto with nat.
+Rewrite H; Elim x; Simpl; Intros; Auto with nat.
+Save.
+Hints Resolve add_sym : nat.
+
+Lemma add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
+Intros x1 x2 y1 y2 eq1 eq2; Rewrite eq1; Rewrite eq2; Auto.
+Save.
+Hints Resolve add_eq_compat : nat.
+
+Lemma add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)).
+Intros x y z; Elim z; Simpl; Intros; Auto with nat.
+Save.
+
+
+
+(*s Lemmas for [one] *)
+Lemma S_0_1 : (S zero)=one.
+Auto.
+Save.
+
+(*s Lemmas for [<], 
+    properties of [>], [<=] and [>=] will be derived from [<] *)
+
+Lemma lt_trans : (x,y,z:N)x<y->y<z->x<z.
+Intros x y z lt1 lt2; Elim lt2; Unfold lt; Auto with nat.
+Save.
+Hints Resolve lt_trans : nat.
+
+Lemma lt_x_Sx : (x:N)x<(S x).
+Unfold lt; Auto with nat.
+Save.
+Hints Resolve lt_x_Sx : nat.
+
+Lemma lt_S_compat : (x,y:N)(x<y)->(S x)<(S y).
+Intros x y lt1; Elim lt1; Unfold lt; Auto with nat.
+Save.
+Hints Resolve lt_S_compat : nat.
+
+Lemma lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
+Intros x1 x2 y1 y2 eq1 eq2; Rewrite eq1; Rewrite eq2; Trivial.
+Save.
+
+Lemma lt_add_compat_l : (x,y,z:N)(x<y)->((x+z)<(y+z)).
+Intros x y z lt1; Elim z; Simpl; Auto with nat.
+Save.
+
+Lemma lt_Sx_Sy_lt : (x,y:N)((S x)<(S y))->(x<y).
+Intros x y lt1; Inversion lt1; EAuto with nat.
+Save.
+Hints Immediate lt_Sx_Sy_lt : nat.
+
+Lemma lt_anti_refl : (x:N)~(x<x).
+Induction x; Red; Intros.
+Inversion H.
+Auto with nat.
+Save.
+
+
+
+  
\ No newline at end of file
diff --git a/theories/Num/Nat/Make b/theories/Num/Nat/Make
new file mode 100644
index 000000000..4e81efed5
--- /dev/null
+++ b/theories/Num/Nat/Make
@@ -0,0 +1,5 @@
+Params.v
+EqAxioms.v
+Axioms.v
+NSyntax.v
+NeqDef.v
\ No newline at end of file
diff --git a/theories/Num/Nat/NSyntax.v b/theories/Num/Nat/NSyntax.v
new file mode 100644
index 000000000..9752dd2e9
--- /dev/null
+++ b/theories/Num/Nat/NSyntax.v
@@ -0,0 +1,26 @@
+
+(*s Syntax for arithmetic *)
+
+Infix 6 "<" lt.
+Infix 6 "<=" le.
+Infix 6 ">" gt.
+Infix 6 ">=" ge.
+
+(*i Infix 7 "+" plus. i*)
+
+Grammar constr lassoc_constr4 :=
+  squash_sum
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
+      case [$c2] of
+        (SQUASH $T2) ->
+            case [$c1] of
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
+            esac
+      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
+      esac.
+
+Syntax constr
+  level 4:
+    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
+.
\ No newline at end of file
diff --git a/theories/Num/Nat/NeqDef.v b/theories/Num/Nat/NeqDef.v
new file mode 100644
index 000000000..8ce7df03a
--- /dev/null
+++ b/theories/Num/Nat/NeqDef.v
@@ -0,0 +1,5 @@
+
+(*s Definition of inequality *)
+
+Require Params.
+Definition neq [x,y:N] := (eqN x y)->False.
\ No newline at end of file
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
new file mode 100644
index 000000000..73375e242
--- /dev/null
+++ b/theories/Num/NeqDef.v
@@ -0,0 +1,9 @@
+
+(*s Definition of inequality *)
+
+Require Params.
+Require EqParams.
+Definition neq [x,y:N] := (eqN x y)->False.
+
+Infix 6 "<>" neq.
+
diff --git a/theories/Num/Params.v b/theories/Num/Params.v
new file mode 100644
index 000000000..a7be171b8
--- /dev/null
+++ b/theories/Num/Params.v
@@ -0,0 +1,20 @@
+(*i $Id $ i*)
+
+(*s 
+  Axiomatisation of a numerical set 
+  It will be instantiated by Z and R later on
+  We choose to introduce many operation to allow flexibility in definition 
+  ([S] is primitive in the definition of [nat] while [add] and [one] 
+   are primitive in the definition 
+*)
+
+Parameter N:Type.
+Parameter zero:N.
+Parameter one:N.
+Parameter add:N->N->N.
+Parameter S:N->N.
+
+(*s Relations, equality is defined separately *)
+Parameter lt,le,gt,ge:N->N->Prop.    
+
+