blob: 12d3ad2fdb446a9f740d108515d9817dd0c40242 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Library for binary natural numbers *)
Require Export BinNums.
Require Export BinPos.
Require Export BinNat.
Require Export Nnat.
Require Export Ndiv_def.
Require Export Nsqrt_def.
Require Export Ngcd_def.
Require Export Ndigits.
Require Export NArithRing.
(** [N] contains an [order] tactic for natural numbers *)
(** Note that [N.order] is domain-agnostic: it will not prove
[1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
Local Open Scope N_scope.
Section TestOrder.
Let test : forall x y, x<=y -> y<=x -> x=y.
Proof.
N.order.
Qed.
End TestOrder.
|
