Z
About Z
We consider the implementation of integers as signed binary sequences (the datatype Z as defined in ZArith, in the standard library).Apartness
We define the apartness as the negation of the Leibniz equality:
Some properties of apartness:
Lemma ap_Z_irreflexive0 : forall x : Z, ~ (x{#Z}x).
Lemma ap_Z_symmetric0 : forall x y : Z, (x{#Z}y) -> y{#Z}x.
Lemma ap_Z_cotransitive0 : forall x y : Z,
(x{#Z}y) -> forall z : Z, (x{#Z}z) or (z{#Z}y).
Lemma ap_Z_tight0 : forall x y : Z, ~ (x{#Z}y) <-> x = y.
Lemma ONE_neq_O : 1{#Z}0.
Lemma Zplus_wd0 : forall x1 x2 y1 y2 : Z,
x1 = x2 -> y1 = y2 -> (x1 + y1)%Z = (x2 + y2)%Z.
Lemma Zplus_strext0 : forall x1 x2 y1 y2 : Z,
(x1 + y1{#Z}x2 + y2) -> (x1{#Z}x2) or (y1{#Z}y2).
Definition posZ (x : Z) : positive :=
match x with
| Z0 => 1%positive
| Zpos p => p
| Zneg p => p
end.
Lemma a_very_specific_lemma1 : forall a b c d e f : Z, c <> 0%Z ->
(a * b)%Z = (c * d)%Z -> (c * e)%Z = (f * b)%Z -> (a * e)%Z = (f * d)%Z.
Lemma a_very_specific_lemma2 : forall a b c d s r t u : Z,
(a * r)%Z = (b * s)%Z -> (c * u)%Z = (d * t)%Z ->
((a * t + c * s) * (r * u))%Z = ((b * u + d * r) * (s * t))%Z.
Lemma a_very_specific_lemma3 : forall (a b c d : Z) (s r t u : positive),
(a * r)%Z = (b * s)%Z -> (c * u)%Z = (d * t)%Z ->
((a * t + c * s) * (r * u)%positive)%Z = ((b * u + d * r) * (s * t)%positive)%Z.
Lemma a_very_specific_lemma4 : forall a b c m n p : Z,
((a * (n * p) + (b * p + c * n) * m) * (m * n * p))%Z =
(((a * n + b * m) * p + c * (m * n)) * (m * (n * p)))%Z.
Lemma a_very_specific_lemma5 : forall (a b c : Z) (m n p : positive),
((a * (n * p)%positive + (b * p + c * n) * m) * (m * n * p)%positive)%Z =
(((a * n + b * m) * p + c * (m * n)%positive) * (m * (n * p))%positive)%Z.
Lemma posZ_pos : forall x : Z, (x > 0)%Z -> posZ x = x :>Z.
Lemma posZ_neg : forall x : Z, (x < 0)%Z -> posZ x = (- x)%Z :>Z.
Lemma posZ_Zsgn : forall x : Z, x <> 0%Z -> (Zsgn x * posZ x)%Z = x.
Lemma posZ_Zsgn2 : forall x : Z, x <> 0%Z -> (Zsgn x * x)%Z = posZ x.
Lemma a_very_specific_lemma5' : forall (m n p : positive) (a b c : Z),
(a * n < b * m)%Z -> (b * p)%Z = (c * n)%Z -> (a * p < c * m)%Z.