proposition: Lemma until_mapmult_permmod : forall (p : nat) (a : Z), Prime p -> ~ Mod a 0 p -> permmod p (until (pred p)) (mapmult a (until (pred p))).
proof: Proof. intros. apply nodoubles_allex_permmod. assumption. unfold mapmult in |- *. apply map_length. apply until_nodoubles. assumption. unfold allex in |- *. intros. apply (until_mapmult_allex p a H H0). assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime