test-suite/output/bug_9370.v


1
2
3
4
5
6
7
8
9
10
11
12

Require Import Reals.
Open Scope R_scope.
Goal 1/1=1.
Proof.
  field_simplify (1/1).
Show.
  field_simplify.
Show.
  field_simplify.
Show.
  reflexivity.
Qed.