proposition: Lemma to_p_nplus: forall x y, (x ++ y):%p = x:%p + y:%p.
proof: Proof. intros x y. unfold nplus, to_p, pkplus, GZnZ.add. unfold pK; apply zirr; simpl. assert (F1:= p_pos). rewrite <- Zmod_div_mod; auto. rewrite Zplus_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