blob: 49442b757ff3f86b5ca054a5d3a05869b6a13e2e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Require ZArith.
Check `32`.
Check [f:nat->Z]`(f O) + 0`.
Check [x:positive]`(POS (xO x))`.
Check [x:positive]`(POS x)+1`.
Check [x:positive]`(POS x)`.
Check [x:positive]`(NEG (xO x))`.
Check [x:positive]`(POS (xO x))+0`.
Check [x:positive]`(Zopp (POS (xO x)))`.
Check [x:positive]`(Zopp (POS (xO x)))+0`.
Check `(inject_nat O)+1`.
Check (Zplus `0` (inject_nat (plus O O))).
Check `(inject_nat O)=0`.
(* Submitted by Pierre Casteran *)
Require Arith.
Check (Zplus `0` (inject_nat (11))).
|
