diff options
| author | Michael Soegtrop | 2020-05-01 14:42:02 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2020-05-01 14:42:02 +0200 |
| commit | f129326d545ae27d362132b279167d119894a992 (patch) | |
| tree | 0b1da21844fcf75dd7090c42e61b3eb677a9a45f /test-suite/complexity | |
| parent | df89e28b0de6597b849078a4fd7d2dce3710f5e4 (diff) | |
| parent | 18544983e1b2a342c8bbcbd3c51003b11453213f (diff) | |
Merge PR #12221: Replace QSeqEquiv by QCauchySeq, simplify proofs.
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'test-suite/complexity')
| -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. |