proposition: Lemma to_p_nsub: forall x y, (x -- y):%p = x:%p - y:%p.
proof: Proof. intros x y. unfold nsub, to_p, pksub, GZnZ.sub. unfold pK; apply zirr; simpl. assert (F1:= p_pos). rewrite <- Zmod_div_mod; auto. rewrite Zminus_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