proposition: Theorem rel_prime_is_inv: forall a, is_inv Z pmult mkZp 1 Z.eq_dec a = if (rel_prime_dec a n) then true else false.
proof: Proof. assert (Hu: 0 < n); try apply Z.lt_trans with 1; auto with zarith. intros a; case (rel_prime_dec a n); intros H. assert (H1: Bezout a n 1); try apply rel_prime_bezout; auto. inversion H1 as [c d Hcd]; clear H1. assert (pmult (c mod n) a = 1). unfold pmult; rewrite Zmult_mod; try rewrite Zmod_mod; auto. rewrite <- Zmult_mod; auto. replace (c * a) with (1 + (-d) * n). rewrite Z_mod_plus; auto with zarith. rewrite Zmod_small; auto with zarith. rewrite <- Hcd; ring. apply is_inv_true with (a := (c mod n)); auto. rewrite pmult_comm; auto. apply mkZp_in; auto with zarith. apply Z_mod_lt; auto with zarith. apply is_inv_false. intros c H1; left; intros H2; contradict H. apply bezout_rel_prime. apply Bezout_intro with c (- (Z.div (c * a) n)). pattern (c * a) at 1; rewrite (Z_div_mod_eq_full (c * a) n). unfold pmult in H2; rewrite (Zmult_comm c); try rewrite H2. ring. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression