blob: f4548bbb2d8019be2d3664acc82dec6321a34846 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: NArithRing.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *)
(* Instantiation of the Ring tactic for the binary natural numbers *)
Require Export Ring.
Require Export ZArith_base.
Require NArith.
Require Eqdep_dec.
Definition Neq := [n,m:entier]
Cases (Ncompare n m) of
EGAL => true
| _ => false
end.
Lemma Neq_prop : (n,m:entier)(Is_true (Neq n m)) -> n=m.
Intros n m H; Unfold Neq in H.
Apply Ncompare_Eq_eq.
NewDestruct (Ncompare n m); [Reflexivity | Contradiction | Contradiction ].
Save.
Definition NTheory : (Semi_Ring_Theory Nplus Nmult (Pos xH) Nul Neq).
Split.
Apply Nplus_comm.
Apply Nplus_assoc.
Apply Nmult_comm.
Apply Nmult_assoc.
Apply Nplus_0_l.
Apply Nmult_1_l.
Apply Nmult_0_l.
Apply Nmult_plus_distr_r.
Apply Nplus_reg_l.
Apply Neq_prop.
Save.
Add Semi Ring entier Nplus Nmult (Pos xH) Nul Neq NTheory [Pos Nul xO xI xH].
|
