diff options
| author | Jasper Hugunin | 2020-08-25 13:37:04 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:33 -0700 |
| commit | b9dd65f8d7d7600693b6d38e52b5b966e8b24db6 (patch) | |
| tree | 3e6ab65de6c35e0dd70b9d088bd4dbb0c72a8bd3 | |
| parent | b8d05916f64136cf809de1fbfd0263a47d192e5e (diff) | |
Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 446ed07b53..4122632603 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -58,7 +58,7 @@ Qed. Lemma sqrt_nonneg : forall a, 0<=√a. Proof. - intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. + intros a. destruct (lt_ge_cases a 0) as [Ha|Ha]. - now rewrite (sqrt_neg _ Ha). - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed. @@ -429,7 +429,7 @@ Qed. Lemma sqrt_up_nonneg : forall a, 0<=√°a. Proof. - intros. destruct (le_gt_cases a 0) as [Ha|Ha]. + intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite sqrt_up_eqn0. - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. Qed. @@ -527,7 +527,7 @@ Lemma sqrt_sqrt_up_exact : forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. - split. - intros. exists √a. + split. - intros H. exists √a. split. + apply sqrt_nonneg. + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b & Hb & Hb'). rewrite Hb'. |