Newer
Older
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
(**
This file is part of the Elfic library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
From Coq Require Import Arith Nat Lia.
Section Order_compl.
(** Complements on the order on natural numbers. **)
Lemma lt_1 :
forall n, n < 1 <-> n = 0.
Proof.
intros; lia.
Qed.
Lemma lt_2 :
forall n, n < 2 <-> n = 0 \/ n = 1.
Proof.
intros; lia.
Qed.
End Order_compl.
Section Mult_compl.
(** Complements on the multiplication on natural numbers. **)
Lemma pred_mul_S :
forall N M, pred (S N * S M) = S N * M + N.
Proof.
intros; lia.
Qed.
Lemma lt_mul_S :
forall N M p, p < S N * S M <-> p < S (pred (S N * S M)).
Proof.
intros; rewrite <- S_pred_pos; try easy.
apply Nat.mul_pos_pos; lia.
Qed.
End Mult_compl.
Section Pow_compl.
(** Complements on the power on natural numbers. **)
Lemma S_pow_pos :
forall N M, 0 < N -> 0 < N ^ M.
Proof.
intros N M HN.
destruct N; try easy; clear HN.
destruct N.
rewrite Nat.pow_1_l; lia.
destruct M.
rewrite Nat.pow_0_r; lia.
apply lt_trans with (S M); try lia.
apply Nat.pow_gt_lin_r; lia.
Qed.
Lemma lt_pow_S :
forall N M p, p < S M ^ S N <-> p < S (pred (S M ^ S N)).
Proof.
intros; rewrite Nat.succ_pred; try easy.
apply Nat.pow_nonzero; lia.
Qed.
(*
Lemma diff_pow :
forall a b N,
a ^ S N - b ^ S N = (a - b) * sum_f_0 (fun n => a ^ n * b ^ (N - n)) N.
Proof.
*)
(*
Lemma pred_pow_S :
forall N M, pred (S M ^ S N) = M * sum_f_0 (pow (S M)) N.
Proof.
intros N M; rewrite <- (pow1 (S N)), diff_pow; f_equal.
rewrite S_INR; lra.
f_equal; apply functional_extensionality; intros n.
rewrite pow1; lra.
Qed.
*)
End Pow_compl.