From 0fd535b57b93bada6cc00c2e372f2f94d2768567 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 18 Jul 2016 09:37:36 -0400 Subject: ported IterAssocOp to use monoid rather than a billion context variables that add up to a monoid --- src/ModularArithmetic/ModularArithmeticTheorems.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 8e526745c..951f848bf 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -220,7 +220,7 @@ 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. + 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]; -- cgit v1.2.3