diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSqrt.v | 10 |
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. |