blob: bc3b01225104ae3a3f4d342fee3c771fb5d27599 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
Require Import Coq.micromega.Lia.
Require Import Coq.ZArith.ZArith.
Local Open Scope Z_scope.
Module Z.
Lemma pow2_ge_0: forall a, (0 <= 2 ^ a)%Z.
Proof.
intros; apply Z.pow_nonneg; omega.
Qed.
Lemma pow2_gt_0: forall a, (0 <= a)%Z -> (0 < 2 ^ a)%Z.
Proof.
intros; apply Z.pow_pos_nonneg; [|assumption]; omega.
Qed.
Lemma pow2_lt_or_divides : forall a b, 0 <= b ->
2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0.
Proof.
intros a b H.
destruct (Z_lt_dec a b); [left|right].
{ apply Z.pow_lt_mono_r; auto; omega. }
{ replace a with (a - b + b) by ring.
rewrite Z.pow_add_r by omega.
apply Z.mod_mul, Z.pow_nonzero; omega. }
Qed.
End Z.
|
