Fermat's Last Theorem for regular primes

This file combines the first and second cases to prove Fermat's Last Theorem at every odd regular prime exponent.

theorem flt_regular {p : ℕ} [Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (hodd : p ≠ 2) : FermatLastTheoremFor p

Fermat's last theorem for regular primes.