ring2.v

From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.

Open Scope ring_scope.

Import  GRing.Theory.

Variable R: numFieldType.

Definition rt :
    @ring_theory R 0%:R 1%:R +%R *%R (fun a b => a - b) -%R eq.
Proof.
    apply mk_rt.
    apply add0r.
    apply addrC.
    apply addrA.
    apply mul1r.
    apply mulrC.
    apply mulrA.
    apply mulrDl.
    by [].
    apply subrr.
Qed.


Add Ring Ringgg : rt.

Lemma tmp2:
    forall x y z:R,  x + y = y + x.
Proof.
    move => x y z.
    Unset Printing Notations.
    Fail ring_simplify.
Qed.