blob: 5569798d54bcc8351c522e1c16ede72ae5ee744d (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Coq.Reals.Reals Coq.nsatz.Nsatz.
Local Open Scope R.
Goal forall x y : R,
x*x = y * y ->
x*x = -y * -y ->
x*(x*x) = 0 -> (* The associativity does not actually matter, *)
(x*x)*x = 0. (* just otherwise [assumption] would solve the goal. *)
Proof.
nsatz.
Qed.
|
