diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-05-18 17:50:48 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-05-18 17:50:48 -0400 |
| commit | 7fcbb62c515ad973f43a43a73f8ea821e63e3ff6 (patch) | |
| tree | 40c39ed7cc0837fb27c00f914d917d69219fbd7a /src/ModularArithmetic/ModularArithmeticTheorems.v | |
| parent | 275fd8922e925e55d279569cebcc6f20bcf302ff (diff) | |
F: pow_nat_iter_op_correct
Diffstat (limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 8b1ae9f93..dabfcf883 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -6,6 +6,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. +Require Export Crypto.Util.IterAssocOp. Section ModularArithmeticPreliminaries. Context {m:Z}. @@ -209,6 +210,14 @@ Section FandZ. reflexivity. Qed. + Lemma pow_nat_iter_op_correct: forall (x:F m) n, (nat_iter_op mul 1) (N.to_nat n) x = x^n. + Proof. + induction n using N.peano_ind; + destruct (F_pow_spec x) as [pow_0 pow_succ]; + rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ; + simpl; congruence. + Qed. + Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m -> b mod m = (- a) mod m. Proof. |