proposition: Lemma to_p_2: 2:%p = 2.
proof: Proof. unfold to_p, pkplus, pkI, GZnZ.add, pK; apply zirr; simpl. assert (F1:= p_pos). rewrite <- Zplus_mod; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod