diff options
| author | Hugo Herbelin | 2019-10-27 19:12:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-10-27 19:12:36 +0100 |
| commit | 943dcfec49b38267488e01cc680fa456739b92cc (patch) | |
| tree | ef23b87facfb11eaee0014ed2dadd5d17ae5b3b0 /test-suite | |
| parent | f508ddcd2cfff152b8d6291d96e4b87ef9fe2ff9 (diff) | |
| parent | c690a68ba0b78b913cbcb60f7508d431071d4c79 (diff) | |
Merge PR #10827: Replace classical reals quotient axioms by functional extensionality
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Nsatz.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 381fbabe72..998f3f7dd1 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -419,13 +419,13 @@ Qed. -Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point, +Lemma Desargues: forall A B C A1 B1 C1 P Q T S:point, X S = 0 -> Y S = 0 -> Y A = 0 -> collinear A S A1 -> collinear B S B1 -> collinear C S C1 -> collinear B1 C1 P -> collinear B C P -> collinear A1 C1 Q -> collinear A C Q -> - collinear A1 B1 R -> collinear A B R -> - collinear P Q R + collinear A1 B1 T -> collinear A B T -> + collinear P Q T \/ X A = X B \/ X A = X C \/ X B = X C \/ X A = 0 \/ Y B = 0 \/ Y C = 0 \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1. Proof. @@ -440,8 +440,8 @@ let lv := rev (X A :: Y A1 :: X A1 :: Y B1 :: Y C1 - :: X R - :: Y R + :: X T + :: Y T :: X Q :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in nsatz with radicalmax :=1%N strategy:=0%Z |