blob: 494cb30dd5307ef13eadf9b634ced5a0333fbab5 (
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
Require Export Arith_base.
Require Import BinInt.
Require Import Zorder.
Require Import Decidable.
Require Import Peano_dec.
Require Export Compare_dec.
Local Open Scope Z_scope.
(***************************************************************)
(** * Moving terms from one side to the other of an inequality *)
Theorem Zne_left n m : Zne n m -> Zne (n + - m) 0.
Proof.
unfold Zne. now rewrite <- Z.sub_move_0_r.
Qed.
Theorem Zegal_left n m : n = m -> n + - m = 0.
Proof.
apply Z.sub_move_0_r.
Qed.
Theorem Zle_left n m : n <= m -> 0 <= m + - n.
Proof.
apply Z.le_0_sub.
Qed.
Theorem Zle_left_rev n m : 0 <= m + - n -> n <= m.
Proof.
apply Z.le_0_sub.
Qed.
Theorem Zlt_left_rev n m : 0 < m + - n -> n < m.
Proof.
apply Z.lt_0_sub.
Qed.
Theorem Zlt_left_lt n m : n < m -> 0 < m + - n.
Proof.
apply Z.lt_0_sub.
Qed.
Theorem Zlt_left n m : n < m -> 0 <= m + -1 + - n.
Proof.
intros. rewrite Z.add_shuffle0. change (-1) with (- Z.succ 0).
now apply Z.le_0_sub, Z.le_succ_l, Z.lt_0_sub.
Qed.
Theorem Zge_left n m : n >= m -> 0 <= n + - m.
Proof.
Z.swap_greater. apply Z.le_0_sub.
Qed.
Theorem Zgt_left n m : n > m -> 0 <= n + -1 + - m.
Proof.
Z.swap_greater. apply Zlt_left.
Qed.
Theorem Zgt_left_gt n m : n > m -> n + - m > 0.
Proof.
Z.swap_greater. apply Z.lt_0_sub.
Qed.
Theorem Zgt_left_rev n m : n + - m > 0 -> n > m.
Proof.
Z.swap_greater. apply Z.lt_0_sub.
Qed.
Theorem Zle_mult_approx n m p :
n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p.
Proof.
Z.swap_greater. intros. Z.order_pos.
Qed.
Theorem Zmult_le_approx n m p :
n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
Proof.
Z.swap_greater. intros. apply Z.lt_succ_r.
apply Z.mul_pos_cancel_r with n; trivial. Z.nzsimpl.
apply Z.le_lt_trans with (m*n+p); trivial.
now apply Z.add_lt_mono_l.
Qed.
|
