proposition: Lemma to_p_pow: forall x n, (x ^ (Z_of_nat n)):%p = pow pkI pkmul (x:%p) n.
proof: Proof. intros x n; elim n; clear n. simpl Z_of_nat; simpl pow; rewrite Zpower_0_r; auto. intros n Hrec; rewrite inj_S; unfold Z.succ; rewrite Zpower_exp; auto with zarith. assert (tmp: forall n x, pow 1 pkmul x (S n) = x * pow 1 pkmul x n). intros n1 x1; case n1; simpl; auto; ring. rewrite tmp; clear tmp. rewrite <- Hrec; rewrite <- to_p_nmul. rewrite Zpower_1_r; rewrite Zmult_comm. unfold to_p, nmul, pkmul, pK; apply zirr; simpl. assert (F1:= p_pos). rewrite <- Zmod_div_mod; auto with zarith. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod