diff options
Diffstat (limited to 'theories/Numbers/Natural/Peano/NPeano.v')
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index b6b26363e..d5df6329a 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -53,6 +53,11 @@ Proof. reflexivity. Qed. Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b. Proof. reflexivity. Qed. +Definition square n := n * n. + +Lemma square_spec n : square n = n * n. +Proof. reflexivity. Qed. + Definition Even n := exists m, n = 2*m. Definition Odd n := exists m, n = 2*m+1. @@ -737,6 +742,9 @@ Definition pow_succ_r := pow_succ_r. Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed. Definition pow := pow. +Definition square := square. +Definition square_spec := square_spec. + Definition log2_spec := log2_spec. Definition log2_nonpos := log2_nonpos. Definition log2 := log2. |