proposition: Theorem Nlittle_fermat_alt : forall a p, Nprime p -> Nrel_prime a p -> (p | a ^ (pred p) - 1).
proof: Proof. intros. destruct p. apply Nnot_prime_0 in H. contradiction. destruct p. apply Nnot_prime_1 in H. contradiction. assert(S(S p)|a^(S(S p))-a). apply Nlittle_fermat. auto. simpl. rewrite Npower_succ in H1. replace (a * a ^ S p - a) with (a * a ^ S p - a*1) in H1. rewrite <- Nat.mul_sub_distr_l in H1. apply Ngauss in H1. auto. apply Nrel_prime_sym. auto. rewrite Nat.mul_1_r. auto. Qed.
imports: Coq(Arith Lia)