ring3.v

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



Import  GRing.Theory.

Variable R: numFieldType.
Open Scope ring_scope.


Definition T:= GRing.Zmodule.sort R.

(* 
Definition addT : T -> T -> T :=
    fun x y => (x + y)%R.
Notation "x ++ y":= (addT x y).

Definition mulT : T -> T -> T :=
    fun x y => (x * y)%R.
Local Notation "x * y":= (mulT x y). *)

Definition subT : T -> T -> T :=
    fun x y => (x - y)%R.
Local Notation "x - y":= (subT x y).


Definition oppT : T -> T :=
    fun x => (-x)%R.
Local Notation "- x":= (oppT x).

Definition rt :
    @ring_theory T 0%R 1%R +%R *%R subT oppT 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.


Set Ltac Backtrace.

Lemma tmp2:
    forall x y z:T,   x + y = y + x.
Proof.
    move => x y z.
    Unset Printing Notations.
    Fail ring.