Library Coq.ZArith.Zcompare
i
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
Relating x ?= y to Zle, Zlt, Zge or Zgt