¿Cómo probar automáticamente la igualdad simple de números reales en Coq?

Lo que estoy buscando es unautotáctica similar que puede probar igualdades simples como:

1/2 = 2/4

Hasta ahora, lo que he intentado manualmente es usarring_simplify yfield_simplify para probar las igualdades. Incluso esto no funciona bien (Coq 8.5b3). El siguiente ejemplo 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. 

Pero era necesario usarfield_simplfy dos veces antes dereflexivity. El primerofield_simplfiy me da

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

que no está sujeto a la reflexividad.

El siguiente ejemplo no funciona,field_simplify parece no hacer nada en el objetivo, y por lo tanto,reflexivity No se puede usar.

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

De nuevo, ¿hay una forma automática de lograr esto, como unfield_auto?

Respuestas a la pregunta(1)

Su respuesta a la pregunta