NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrt

   Some more results about sqrt. Similar results for sqrt_up.

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

2 files changed, 10 insertions, 9 deletions

diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 9af668487f..8df64756ac 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -492,14 +492,5 @@ eapply le_trans; [ | eapply half_upper_bound ].
 apply mul_le_mono_l; auto.
 Qed.
 
-(** Later:
-
-Theorem log_mul : forall n m, 0 < n -> 0 < m ->
- log (n*m) == log n + log m.
-
-Theorem log_pow2 : forall n, log (2^^n) = n.
-
-*)
-
 End NdefOpsProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index 4a9cf536be..1b49678e42 100644
--- a/theories/Numbers/Natural/Abstract/NSqrt.v
+++ b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -56,10 +56,20 @@ Definition sqrt_mul_below : forall a b, √a * √b <= √(a*b)
 Lemma sqrt_mul_above : forall a b, √(a*b) < S (√a) * S (√b).
 Proof. wrap sqrt_mul_above. Qed.
 
+Lemma sqrt_succ_le : forall a, √(S a) <= S (√a).
+Proof. wrap sqrt_succ_le. Qed.
+
+Lemma sqrt_succ_or : forall a, √(S a) == S (√a) \/ √(S a) == √a.
+Proof. wrap sqrt_succ_or. Qed.
+
 Definition sqrt_add_le : forall a b, √(a+b) <= √a + √b
  := sqrt_add_le.
 
 Lemma add_sqrt_le : forall a b, √a + √b <= √(2*(a+b)).
 Proof. wrap add_sqrt_le. Qed.
 
+(** For the moment, we include stuff about [sqrt_up] with patching them. *)
+
+Include NZSqrtUpProp A A B NZSqrtP.
+
 End NSqrtProp.