test-suite/bugs/closed/bug_12860.v


1
2
3
4
5
6
7
8
9
10

Require Import Coq.nsatz.NsatzTactic.
Require Import Coq.ZArith.ZArith Coq.QArith.QArith.

Goal forall x y : Z, (x + y = y + x)%Z.
  intros; nsatz.
Qed.

Goal forall x y : Q, Qeq (x + y) (y + x).
  intros; nsatz.
Qed.