Library Coq.ZArith.Zcomplements
About parity
The biggest power of 2 that is stricly less than a
Easy to compute: replace all "1" of the binary representation by
"0", except the first "1" (or the first one :-)
Two more induction principles over Z.
Theorem Z_lt_abs_rec :
forall P:Z ->
Set,
(
forall n:Z, (
forall m:Z,
Zabs m <
Zabs n ->
P m) ->
P n) ->
forall n:Z,
P n.
Theorem Z_lt_abs_induction :
forall P:Z ->
Prop,
(
forall n:Z, (
forall m:Z,
Zabs m <
Zabs n ->
P m) ->
P n) ->
forall n:Z,
P n.
To do case analysis over the sign of z
Lemma Zcase_sign :
forall (
n:Z) (
P:Prop), (
n = 0 ->
P) -> (
n > 0 ->
P) -> (
n < 0 ->
P) ->
P.
Lemma sqr_pos :
forall n:Z,
n *
n >= 0.
A list length in Z, tail recursive.