Matita Home

`ring `

- Synopsis:
**ring**- Pre-conditions:
The conclusion of the current sequent must be an equality over Coq's real numbers that can be proved using the ring properties of the real numbers only.

- Action:
It closes the current sequent veryfying the equality by means of computation (i.e. this is a reflexive tactic, implemented exploiting the "two level reasoning" technique).

- New sequents to prove:
None.