Helper

expr_modr

Section BenalohEuler

Type Lemma

Proof Lines 4

Lemma expr_modr (k : nat) : (val y) ^+ k = (val y) ^+ (k %% r)%N.

Exponentiation of y depends only on exponent mod r

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...