File: test_4_0.v

package info (click to toggle)
coq-hierarchy-builder 1.10.1-2
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 2,216 kB
  • sloc: makefile: 132
file content (17 lines) | stat: -rw-r--r-- 448 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
From Coq Require Import ZArith ssreflect.
From HB Require Import structures.
From HB Require Import demo1.hierarchy_4.

HB.instance
Definition Z_ring_axioms :=
  Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul
    Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l
    Z.mul_assoc Z.mul_1_l Z.mul_1_r
    Z.mul_add_distr_r Z.mul_add_distr_l.



Open Scope hb_scope.

Example test1 (m n : Z) : (m + n) - n + 0 = m.
Proof. by rewrite addrNK addr0. Qed.