proposition: Lemma until_mapmult_allex : forall (p : nat) (a : Z), Prime p -> ~ Mod a 0 p -> allex p (until (pred p)) (mapmult a (until (pred p))).
proof: Proof. unfold allex in |- *. intros p a Hprime Ha0 x Hx. elim Hprime. intros Hp Hp1. elim (mod_mult_inv_r a p). intros ra Hra. elim (zdiv_rem (Z_of_nat p) (ra * x)). intros q Hq. elim Hq. intros r Hr. elim Hr. intros. elim H. intros. split with (a * r)%Z. split. apply mapmult_image. apply until_ok. split. elim (Zle_lt_or_eq 0 r). intro. assumption. intro. rewrite <- H3 in H0. rewrite <- Zplus_0_r_reverse in H0. elim until_not_0mod with p x. apply lt_trans with 1. apply lt_n_Sn. assumption. assumption. apply mod_mult_cancel_r with (a * ra)%Z. assumption. intro. elim mod_0not1 with p. assumption. apply mod_trans with (a * ra)%Z. apply mod_sym. assumption. assumption. rewrite (Zmult_comm a ra). rewrite Zmult_assoc. rewrite (Zmult_comm x ra). rewrite H0. simpl in |- *. unfold Mod in |- *. split with (q * a)%Z. simpl in |- *. rewrite Zmult_assoc. rewrite (Zmult_comm q). reflexivity. assumption. apply Zlt_succ_le. rewrite <- Znat.inj_S. rewrite <- (S_pred p 1). assumption. assumption. apply mod_mult_cancel_r with ra. assumption. intro. elim mod_0not1 with p. assumption. apply mod_trans with (ra * a)%Z. change (Mod (0 * a) (ra * a) p) in |- *. apply mod_mult_compat. apply mod_sym. assumption. apply mod_refl. rewrite (Zmult_comm ra a). assumption. rewrite (Zmult_comm x ra). rewrite H0. rewrite (Zmult_comm a r). rewrite (Zmult_assoc_reverse r a ra). apply mod_trans with r. split with q. rewrite Zplus_comm. rewrite Zmult_comm. reflexivity. pattern r at 1 in |- *. rewrite <- Zmult_1_l with r. rewrite (Zmult_comm 1 r). apply mod_mult_compat. apply mod_refl. apply mod_sym. assumption. change (Z_of_nat p > Z_of_nat 0)%Z in |- *. apply Znat.inj_gt. apply gt_trans with 1. assumption. apply gt_Sn_n. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime