diff options
| author | Vincent Semeria | 2020-04-30 18:27:21 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2020-04-30 23:21:29 +0200 |
| commit | 18544983e1b2a342c8bbcbd3c51003b11453213f (patch) | |
| tree | 4b32a5440e9e0b510f66f62ba5af9033b915fba5 /test-suite/complexity/ConstructiveCauchyRealsPerformance.v | |
| parent | c4a24b7a7844789a08dabe8a76b20c239a8b8218 (diff) | |
Replace QSeqEquiv by QCauchySeq, simplify proofs.
Force Cauchy modulus equal to identity, make division transparent
Fix test
Diffstat (limited to 'test-suite/complexity/ConstructiveCauchyRealsPerformance.v')
| -rw-r--r-- | test-suite/complexity/ConstructiveCauchyRealsPerformance.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v index c901334da9..f3bc1767da 100644 --- a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v +++ b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v @@ -105,7 +105,7 @@ Proof. Qed. Lemma approx_sqrt_Q_cauchy : - forall q:Q, QCauchySeq (approx_sqrt_Q q) id. + forall q:Q, QCauchySeq (approx_sqrt_Q q). Proof. intro q. destruct q as [k j]. destruct k. - intros n a b H H0. reflexivity. |