∀ p a, prime p ⇒ ¬(p | a) ⇒ permut (λn. mod (a × n) p) (p-1)

Theorem permut_mod : forall (p:nat.nat), forall (a:nat.nat), (primes.prime p) -> (connectives.Not (primes.divides p a)) -> permutation.permut (fun (n:nat.nat) => div_mod.mod (nat.times a n) p) (nat.pred p).

theorem permut_mod : \forall (p:nat). \forall (a:nat). ((prime) p) -> ((Not) ((divides) p a)) -> (permut) (\lambda n : nat. (mod) ((times) a n) p) ((pred) p).

theorem permut_mod : forall (p:nat.nat) , forall (a:nat.nat) , (((primes.prime) ) (p)) -> (((connectives.Not) ) ((((primes.divides) ) (p)) (a))) -> (((permutation.permut) ) (fun (n : nat.nat) , (((div_mod.mod) ) ((((nat.times) ) (a)) (n))) (p))) (((nat.pred_) ) (p)).

permut_mod : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(a:nat_sttfa_th.sttfa_nat):(primes_sttfa_th.prime(p) => (connectives_sttfa_th.sttfa_Not(primes_sttfa_th.sttfa_divides(p)(a)) => permutation_sttfa_th.permut((LAMBDA(n:nat_sttfa_th.sttfa_nat):div_mod_sttfa_th.mod(nat_sttfa_th.times(a)(n))(p)))(nat_sttfa_th.pred(p))))))

Printing for OpenTheory is not working at the moment.