blob: 8f4d5c4fa46912f62d4e8d6c34d7e04562f2a659 (
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
27
28
29
30
31
32
|
Require Import PArith.
Require Import ZArith.
Require Import Lia.
Lemma Pos_pow_1_r: forall p : positive,
(1^p = 1)%positive.
Proof.
intros p.
assert (forall q:positive, Pos.iter id 1 q = 1)%positive as H1.
{ intros q; apply Pos.iter_invariant; tauto. }
induction p.
- cbn; rewrite IHp, H1; reflexivity.
- cbn; rewrite IHp, H1; reflexivity.
- reflexivity.
Qed.
Lemma Pos_le_multiple : forall n p : positive, (n <= p * n)%positive.
Proof.
intros n p.
rewrite <- (Pos.mul_1_l n) at 1.
apply Pos.mul_le_mono_r.
destruct p; discriminate.
Qed.
Lemma Pos_pow_le_mono_r : forall a b c : positive,
(b <= c)%positive
-> (a ^ b <= a ^ c)%positive.
Proof.
intros a b c.
pose proof Z.pow_le_mono_r (Z.pos a) (Z.pos b) (Z.pos c).
lia.
Qed.
|
