proposition: Lemma mod_mult_inv_r : forall (a : Z) (p : nat), Prime p -> ~ Mod a 0 p -> exists ra : Z, Mod (a * ra) 1 p.
proof: Proof. intros. elim (prime_div_or_gcd1 p a). intro. elim H0. elim H1. intros. split with x. simpl in |- *. assumption. intro. elim (gcd_lincomb (Z_of_nat p) a 1). intro alpha. intros. elim H2. intro beta. intros. unfold Mod in |- *. split with beta. split with (- alpha)%Z. simpl in H3. rewrite H3. rewrite (Zplus_comm (Z_of_nat p * alpha)). rewrite Zplus_assoc_reverse. rewrite <- Zmult_plus_distr_r. rewrite Zplus_opp_r. rewrite <- Zmult_0_r_reverse. rewrite <- Zplus_0_r_reverse. reflexivity. apply Zgt_neq. change (Z_of_nat p > Z_of_nat 0)%Z in |- *. apply Znat.inj_gt. apply gt_trans with 1. elim H. intros. assumption. unfold gt in |- *. unfold lt in |- *. apply le_n. assumption. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo gcd