Library Coq.ZArith.Zcompare
Binary Integers (Pierre Crégut, CNET, Lannion, France)
Require Export BinPos.
Require Export BinInt.
Require Import Lt.
Require Import Gt.
Require Import Plus.
Require Import Mult.
Open Local Scope Z_scope.
Transitivity of comparison
Comparison first-order specification
Multiplication and comparison
Reverting x ?= y to trichotomy
Lemma rename :
forall (
A:Type) (
P:A ->
Prop) (
x:A), (
forall y:A,
x =
y ->
P y) ->
P x.
Lemma Zcompare_elim :
forall (
c1 c2 c3:Prop) (
n m:Z),
(
n =
m ->
c1) ->
(
n <
m ->
c2) ->
(
n >
m ->
c3) ->
match n ?=
m with
|
Eq =>
c1
|
Lt =>
c2
|
Gt =>
c3
end.
Lemma Zcompare_eq_case :
forall (
c1 c2 c3:Prop) (
n m:Z),
c1 ->
n =
m ->
match n ?=
m with
|
Eq =>
c1
|
Lt =>
c2
|
Gt =>
c3
end.
Decompose an egality between two ?= relations into 3 implications
Lemma Zcompare_egal_dec :
forall n m p q:Z,
(
n <
m ->
p <
q) ->
((
n ?=
m) =
Eq -> (
p ?=
q) =
Eq) ->
(
n >
m ->
p >
q) -> (
n ?=
m) = (
p ?=
q).
Relating x ?= y to Zle, Zlt, Zge or Zgt