1
Require Import Relations.
3
Require Import Ring_theory.
4
Require Import Ring_base.
8
Variable Rone Rzero : R.
9
Variable Rplus Rmult Rminus : R -> R -> R.
10
Variable Rneg : R -> R.
12
Lemma my_ring_theory : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq
16
Variable Req : R -> R -> Prop.
18
Hypothesis Req_refl : reflexive _ Req.
19
Hypothesis Req_sym : symmetric _ Req.
20
Hypothesis Req_trans : transitive _ Req.
23
reflexivity proved by Req_refl
24
symmetry proved by Req_sym
25
transitivity proved by Req_trans
28
Add Ring my_ring : my_ring_theory (abstract).