proposition: Lemma nopp_correct: forall a1 p1, a1 =~~= p1 -> [[(a1,1%Z)]] -> nopp a1 =~~= opp p1.
proof: Proof. assert (F0: 0 < p); auto with zarith. intros a1 p1 H; inversion_clear H; simpl; constructor; auto. rewrite <- H2. field_simplify_eq; auto. unfold ninv, pkopp, GZnZ.opp, to_p, pK; apply zirr. simpl; rewrite <- Zmod_div_mod; auto with zarith. pattern y at 1; rewrite (Z_div_mod_eq_full y p). rewrite Zopp_plus_distr. rewrite Zopp_mult_distr_r. rewrite Zmult_comm; rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. inversion_clear H. case (inversible_mult_inv _ _ H3); intros _ H4. intros H5; apply (@inversible_kO z 0); auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod