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.
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.