O que estou procurando é umautotática-like que pode provar igualdades simples como:

1/2 = 2/4

Até agora, o que eu tentei manualmente é usarring_simplify efield_simplify para provar a igualdade. Mesmo isso não funciona bem (Coq 8.5b3). O exemplo abaixo funciona:

Require Export Coq.Reals.RIneq.
Local Open Scope Z_scope.
Local Open Scope R_scope.

Example test2: 1 = 1 / 1.
Proof. field_simplify. field_simplify. reflexivity.
Qed. 

Mas era necessário usarfield_simplfy duas vezes antesreflexivity. O primeirofield_simplfiy me dá:

1 subgoal
______________________________________(1/1)
1 / 1 = 1 / 1 / (1 / 1)

que não está sujeito à reflexividade.

O exemplo abaixo não funciona,field_simplify parece não fazer nada no objetivo e, portanto,reflexivity não pode ser usado.

Example test3: 1/2 = 2/4.
Proof. field_simplify. reflexivity. 

Novamente, existe uma maneira automática de conseguir isso, como umfield_auto?