diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-10-25 18:23:02 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-10-25 18:23:02 -0400 |
| commit | d655b90707449b7ebb2aa661fef6d947d9d88c58 (patch) | |
| tree | c2b1cc27073209afb17c0c2323914a6f0dcba26b | |
| parent | 277fbcc216245a32e11044c5794f57f68591bb42 (diff) | |
pos_pow_nat_pos
| -rw-r--r-- | src/Galois/BaseSystem.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index b60a16fb2..036b9d5b1 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -45,7 +45,11 @@ Local Open Scope Z. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. -Admitted. + do 2 (intros; induction n; subst; simpl in *; auto with zarith). + SearchAbout Pos.succ. + rewrite <- Pos.add_1_r, Zpower_pos_is_exp. + apply Zmult_gt_0_compat; auto; compute; auto. +Qed. Module Type BaseCoefs. (** [BaseCoefs] represent the weights of each digit in a positional number system, with the weight of least significant digit presented first. The following requirements on the base are preconditions for using it with BaseSystem. *) |