proposition: Lemma to_p_nmul: forall x y, (x ** y):%p = x:%p * y:%p.
proof: Proof. intros x y. unfold nmul, to_p, pkmul, mul. unfold pK; apply zirr; simpl. assert (F1:= p_pos). rewrite <- Zmod_div_mod; auto. rewrite Zmult_mod; auto. generalize N_lt_2; auto with zarith. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod