Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+โ Ctrl+โ to navigate,
Ctrl+๐ฑ๏ธ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
! This file was ported from Lean 3 source module data.nat.prime
! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Associated
import Mathlib.Algebra.Parity
import Mathlib.Data.Int.Dvd.Basic
import Mathlib.Data.Int.Units
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Nat.Sqrt
import Mathlib.Order.Bounds.Basic
/-!
# Prime numbers
This file deals with prime numbers: natural numbers `p โฅ 2` whose only divisors are `p` and `1`.
## Important declarations
- `Nat.Prime`: the predicate that expresses that a natural number `p` is prime
- `Nat.Primes`: the subtype of natural numbers that are prime
- `Nat.minFac n`: the minimal prime factor of a natural number `n โ 1`
- `Nat.exists_infinite_primes`: Euclid's theorem that there exist infinitely many prime numbers.
This also appears as `Nat.not_bddAbove_setOf_prime` and `Nat.infinite_setOf_prime` (the latter
in `Data.Nat.PrimeFin`).
- `Nat.prime_iff`: `Nat.Prime` coincides with the general definition of `Prime`
- `Nat.irreducible_iff_nat_prime`: a non-unit natural number is
only divisible by `1` iff it is prime
-/
open Bool Subtype
open Nat
namespace Nat
/-- `Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`. -/
-- Porting note: removed @[pp_nodot]
def Prime : (p : โ ) โ ?m.5 p Prime ( p : โ ) :=
Irreducible p
#align nat.prime Nat.Prime
theorem irreducible_iff_nat_prime ( a : โ ) : Irreducible a โ Nat.Prime a :=
Iff.rfl
#align irreducible_iff_nat_prime Nat.irreducible_iff_nat_prime
theorem not_prime_zero : ยฌ Prime 0
| h => h . ne_zero rfl : โ {ฮฑ : Sort ?u.130} {a : ฮฑ }, a = a
#align nat.not_prime_zero Nat.not_prime_zero
theorem not_prime_one : ยฌ Prime 1
| h => h . ne_one rfl : โ {ฮฑ : Sort ?u.179} {a : ฮฑ }, a = a
#align nat.not_prime_one Nat.not_prime_one
theorem Prime.ne_zero { n : โ } ( h : Prime n ) : n โ 0 :=
Irreducible.ne_zero h
#align nat.prime.ne_zero Nat.Prime.ne_zero : โ {n : โ }, Prime n n โ 0
theorem Prime.pos { p : โ } ( pp : Prime p ) : 0 < p :=
Nat.pos_of_ne_zero : โ {n : โ }, n โ 0 0 < n pp . ne_zero
#align nat.prime.pos Nat.Prime.pos : โ {p : โ }, Prime p 0 < p
theorem Prime.two_le : โ { p : โ }, Prime p โ 2 โค p
| 0 , h => ( not_prime_zero h ). elim
| 1 , h => ( not_prime_one h ). elim
| _ + 2, _ => le_add_self
#align nat.prime.two_le Nat.Prime.two_le
theorem Prime.one_lt : โ {p : โ }, Prime p 1 < p Prime.one_lt { p : โ } : Prime p โ 1 < p :=
Prime.two_le
#align nat.prime.one_lt Nat.Prime.one_lt : โ {p : โ }, Prime p 1 < p
instance Prime.one_lt' ( p : โ ) [ hp : Fact p . Prime ] : Fact ( 1 < p ) :=
โจ hp . 1 . one_lt โฉ
#align nat.prime.one_lt' Nat.Prime.one_lt'
theorem Prime.ne_one { p : โ } ( hp : p . Prime ) : p โ 1 :=
hp . one_lt . ne' : โ {ฮฑ : Type ?u.866} [inst : Preorder ฮฑ x y : ฮฑ }, x < y y โ x
#align nat.prime.ne_one Nat.Prime.ne_one : โ {p : โ }, Prime p p โ 1
theorem Prime.eq_one_or_self_of_dvd : โ {p : โ }, Prime p โ (m : โ ), m โฃ p m = 1 โจ m = p Prime.eq_one_or_self_of_dvd { p : โ } ( pp : p . Prime ) ( m : โ ) ( hm : m โฃ p ) :
m = 1 โจ m = p := by
obtain โจ n , hn โฉ := hm
have := pp . isUnit_or_isUnit hn
rw [ Nat.isUnit_iff , Nat.isUnit_iff ] at this
apply Or.imp_right : โ {b c a : Prop }, (b โ c a โจ b a โจ c _ this
rintro rfl
rw [ hn , mul_one ]
#align nat.prime.eq_one_or_self_of_dvd Nat.Prime.eq_one_or_self_of_dvd : โ {p : โ }, Prime p โ (m : โ ), m โฃ p m = 1 โจ m = p
theorem prime_def_lt'' { p : โ } : Prime p โ 2 โค p โง โ ( m ) ( _ : m โฃ p ), m = 1 โจ m = p := by
refine' โจ fun h => โจ h . two_le , h . eq_one_or_self_of_dvd โฉ, fun h => _ โฉ
-- Porting note: needed to make โ explicit
have h1 := (@ one_lt_two โ ..). trans_le : โ {ฮฑ : Type ?u.1729} [inst : Preorder ฮฑ a b c : ฮฑ }, a < b b โค c a < c trans_le h . 1
refine' โจ mt : โ {a b : Prop }, (a โ b ยฌ b ยฌ a Nat.isUnit_iff . mp : โ {a b : Prop }, (a โ b a โ b h1 . ne' : โ {ฮฑ : Type ?u.1840} [inst : Preorder ฮฑ x y : ฮฑ }, x < y y โ x , fun a b hab => _ โฉ
simp only [ Nat.isUnit_iff ]
apply Or.imp_right : โ {b c a : Prop }, (b โ c a โจ b a โจ c _ ( h . 2 a _ )
ยท rintro rfl
rw [ โ mul_right_inj' ( pos_of_gt h1 ). ne' : โ {ฮฑ : Type ?u.2004} [inst : Preorder ฮฑ x y : ฮฑ }, x < y y โ x ne' , โ hab , mul_one ]
ยท rw [ hab ]
exact dvd_mul_right _ _
#align nat.prime_def_lt'' Nat.prime_def_lt''
theorem prime_def_lt { p : โ } : Prime p โ 2 โค p โง โ m < p , m โฃ p โ m = 1 :=
prime_def_lt'' . trans <|
and_congr_right : โ {a b c : Prop }, (a โ (b โ c a โง b โ a โง c fun p2 =>
forall_congr' : โ {ฮฑ : Sort ?u.2378} {p q : ฮฑ โ Prop (โ (a : ฮฑ ), p a โ q a ) โ ((โ (a : ฮฑ ), p a ) โ โ (a : ฮฑ ), q a ) fun _ =>
โจ fun h l d => ( h d ). resolve_right : โ {a b : Prop }, a โจ b ยฌ b a resolve_right ( ne_of_lt : โ {a b : โ }, a < b a โ b l ), fun h d =>
( le_of_dvd : โ {m n : โ }, 0 < n m โฃ n m โค n ( le_of_succ_le p2 ) d ). lt_or_eq_dec . imp_left : โ {a b c : Prop }, (a โ b a โจ c b โจ c imp_left fun l => h l d โฉ
#align nat.prime_def_lt Nat.prime_def_lt
theorem prime_def_lt' { p : โ } : Prime p โ 2 โค p โง โ m , 2 โค m โ m < p โ ยฌ m โฃ p :=
prime_def_lt . trans <|
and_congr_right : โ {a b c : Prop }, (a โ (b โ c a โง b โ a โง c fun p2 =>
forall_congr' : โ {ฮฑ : Sort ?u.2747} {p q : ฮฑ โ Prop (โ (a : ฮฑ ), p a โ q a ) โ ((โ (a : ฮฑ ), p a ) โ โ (a : ฮฑ ), q a ) fun m =>
โจ fun h m2 l d => not_lt_of_ge : โ {ฮฑ : Type ?u.2786} [inst : Preorder ฮฑ a b : ฮฑ }, a โฅ b ยฌ a < b m2 (( h l d ). symm : โ {ฮฑ : Sort ?u.2842} {a b : ฮฑ }, a = b b = a symm โธ by decide ), fun h l d => by
rcases m with ( _ | _ | m )
ยท rw [ eq_zero_of_zero_dvd d ] at p2
revert p2
decide
ยท rfl
ยท exact ( h le_add_self l ). elim : โ {a : Prop } {ฮฑ : Sort ?u.3228}, ยฌ a a โ ฮฑ elim d โฉ
#align nat.prime_def_lt' Nat.prime_def_lt'
theorem prime_def_le_sqrt { p : โ } : Prime p โ 2 โค p โง โ m , 2 โค m โ m โค sqrt p โ ยฌ m โฃ p :=
prime_def_lt' . trans <|
and_congr_right : โ {a b c : Prop }, (a โ (b โ c a โง b โ a โง c fun p2 =>
โจ fun a m m2 l => a m m2 <| lt_of_le_of_lt : โ {ฮฑ : Type ?u.3501} [inst : Preorder ฮฑ a b c : ฮฑ }, a โค b b < c a < c l <| sqrt_lt_self : โ {n : โ }, 1 < n sqrt n < n p2 , fun a =>
have : โ { m k : โ }, m โค k โ 1 < m โ p โ m * k := fun { m k } mk m1 e =>
a m m1 ( le_sqrt . 2 : โ {a b : Prop }, (a โ b b โ a ( e . symm : โ {ฮฑ : Sort ?u.3718} {a b : ฮฑ }, a = b b = a โธ Nat.mul_le_mul_left : โ {n m : โ } (k : โ ), n โค m k * n โค k * m m mk )) โจ k , e โฉ
fun m m2 l โจ k , e โฉ => by
cases' le_total m k with mk km
ยท exact this : โ {m k : โ }, m โค k 1 < m p โ m * k this mk m2 e
ยท rw [ mul_comm ] at e
refine' this : โ {m k : โ }, m โค k 1 < m p โ m * k this km ( lt_of_mul_lt_mul_right _ : ?m.4080 * ?m.4079 < ?m.4081 * ?m.4079 ( zero_le : โ (n : โ ), 0 โค n m )) e
rwa [ one_mul , โ e ] โฉ
#align nat.prime_def_le_sqrt Nat.prime_def_le_sqrt
theorem prime_of_coprime ( n : โ ) ( h1 : 1 < n ) ( h : โ m < n , m โ 0 โ n . coprime m ) : Prime n := by
refine' prime_def_lt . mpr : โ {a b : Prop }, (a โ b b โ a โจ h1 , fun m mlt mdvd => _ โฉ
have hm : m โ 0 := by
rintro rfl
rw [ zero_dvd_iff ] at mdvd
exact mlt . ne' : โ {ฮฑ : Type ?u.4752} [inst : Preorder ฮฑ x y : ฮฑ }, x < y y โ x mdvd
exact ( h m mlt hm ). symm . eq_one_of_dvd mdvd
#align nat.prime_of_coprime Nat.prime_of_coprime
section
/-- This instance is slower than the instance `decidablePrime` defined below,
but has the advantage that it works in the kernel for small values.
If you need to prove that a particular number is prime, in any case
you should not use `by decide`, but rather `by norm_num`, which is
much faster.
-/
@[ local instance ]
def decidablePrime1 ( p : โ ) : Decidable ( Prime p ) :=
decidable_of_iff' _ prime_def_lt'
#align nat.decidable_prime_1 Nat.decidablePrime1
theorem prime_two : Prime 2 := by decide
#align nat.prime_two Nat.prime_two
theorem prime_three : Prime 3 := by decide
#align nat.prime_three Nat.prime_three
theorem Prime.five_le_of_ne_two_of_ne_three : โ {p : โ }, Prime p p โ 2 p โ 3 5 โค p Prime.five_le_of_ne_two_of_ne_three { p : โ } ( hp : p . Prime ) ( h_two : p โ 2 )
( h_three : p โ 3 ) : 5 โค p := by
by_contra' h
revert h_two h_three hp
-- Porting note: was `decide!`
match p with
| 0 => decide
| 1 => decide
| 2 => decide
| 3 => decide
| 4 => decide
| n + 5 => exact ( h . not_le le_add_self ). elim
#align nat.prime.five_le_of_ne_two_of_ne_three Nat.Prime.five_le_of_ne_two_of_ne_three : โ {p : โ }, Prime p p โ 2 p โ 3 5 โค p
end
theorem Prime.pred_pos { p : โ } ( pp : Prime p ) : 0 < pred p :=
lt_pred_iff . 2 : โ {a b : Prop }, (a โ b b โ a pp . one_lt
#align nat.prime.pred_pos Nat.Prime.pred_pos
theorem succ_pred_prime { p : โ } ( pp : Prime p ) : succ ( pred p ) = p :=
succ_pred_eq_of_pos pp . pos
#align nat.succ_pred_prime Nat.succ_pred_prime
theorem dvd_prime { p m : โ } ( pp : Prime p ) : m โฃ p โ m = 1 โจ m = p :=
โจ fun d => pp . eq_one_or_self_of_dvd m d , fun h =>
h . elim : โ {a b c : Prop }, a โจ b (a โ c (b โ c c ( fun e => e . symm : โ {ฮฑ : Sort ?u.7672} {a b : ฮฑ }, a = b b = a โธ one_dvd : โ {ฮฑ : Type ?u.7683} [inst : Monoid ฮฑ a : ฮฑ ), 1 โฃ a _ ) fun e => e . symm : โ {ฮฑ : Sort ?u.7746} {a b : ฮฑ }, a = b b = a โธ dvd_rfl : โ {ฮฑ : Type ?u.7754} [inst : Monoid ฮฑ a : ฮฑ }, a โฃ a โฉ
#align nat.dvd_prime Nat.dvd_prime
theorem dvd_prime_two_le { p m : โ } ( pp : Prime p ) ( H : 2 โค m ) : m โฃ p โ m = p :=
( dvd_prime pp ). trans <| or_iff_right_of_imp : โ {a b : Prop }, (a โ b a โจ b โ b <| Not.elim : โ {a : Prop } {ฮฑ : Sort ?u.7884}, ยฌ a a โ ฮฑ <| ne_of_gt : โ {a b : โ }, b < a a โ b H
#align nat.dvd_prime_two_le Nat.dvd_prime_two_le
theorem prime_dvd_prime_iff_eq { p q : โ } ( pp : p . Prime ) ( qp : q . Prime ) : p โฃ q โ p = q :=
dvd_prime_two_le qp ( Prime.two_le pp )
#align nat.prime_dvd_prime_iff_eq Nat.prime_dvd_prime_iff_eq
theorem Prime.not_dvd_one { p : โ } ( pp : Prime p ) : ยฌ p โฃ 1 :=
Irreducible.not_dvd_one pp
#align nat.prime.not_dvd_one Nat.Prime.not_dvd_one
theorem not_prime_mul : โ {a b : โ }, 1 < a 1 < b ยฌ Prime (a * b not_prime_mul { a b : โ } ( a1 : 1 < a ) ( b1 : 1 < b ) : ยฌ Prime ( a * b ) := fun h =>
ne_of_lt : โ {a b : โ }, a < b a โ b ( Nat.mul_lt_mul_of_pos_left : โ {n m k : โ }, n < m k > 0 k * n < k * m b1 ( lt_of_succ_lt : โ {n m : โ }, succ n < m n < m a1 )) <| by
simpa using ( dvd_prime_two_le h a1 ). 1 : โ {a b : Prop }, (a โ b a โ b ( dvd_mul_right _ _ )
#align nat.not_prime_mul Nat.not_prime_mul : โ {a b : โ }, 1 < a 1 < b ยฌ Prime (a * b
theorem not_prime_mul' : โ {a b n : โ }, a * b = n 1 < a 1 < b ยฌ Prime n not_prime_mul' { a b n : โ } ( h : a * b = n ) ( hโ : 1 < a ) ( hโ : 1 < b ) : ยฌ Prime n := by
a, b, n : โ h : a * b = n hโ : 1 < a hโ : 1 < b rw [ a, b, n : โ h : a * b = n hโ : 1 < a hโ : 1 < b โ h a, b, n : โ h : a * b = n hโ : 1 < a hโ : 1 < b ] a, b, n : โ h : a * b = n hโ : 1 < a hโ : 1 < b
a, b, n : โ h : a * b = n hโ : 1 < a hโ : 1 < b exact not_prime_mul : โ {a b : โ }, 1 < a 1 < b ยฌ Prime (a * b hโ hโ
#align nat.not_prime_mul' Nat.not_prime_mul' : โ {a b n : โ }, a * b = n 1 < a 1 < b ยฌ Prime n
theorem prime_mul_iff { a b : โ } : Nat.Prime ( a * b ) โ a . Prime โง b = 1 โจ b . Prime โง a = 1 := by
simp only [ iff_self_iff , irreducible_mul_iff , โ irreducible_iff_nat_prime , Nat.isUnit_iff ]
#align nat.prime_mul_iff Nat.prime_mul_iff
theorem Prime.dvd_iff_eq { p a : โ } ( hp : p . Prime ) ( a1 : a โ 1 ) : a โฃ p โ p = a := by
refine'
โจ _ , by
rintro rfl
rfl โฉ
rintro โจ j , rfl โฉ
rcases prime_mul_iff . mp : โ {a b : Prop }, (a โ b a โ b hp with ( โจ _ , rfl โฉ | โจ _ , rfl โฉ ) intro.inl.intro intro.inr.intro
ยท intro.inl.intro intro.inr.intro exact mul_one _
ยท exact ( a1 rfl : โ {ฮฑ : Sort ?u.9470} {a : ฮฑ }, a = a ). elim
#align nat.prime.dvd_iff_eq Nat.Prime.dvd_iff_eq
section MinFac
theorem minFac_lemma ( n k : โ ) ( h : ยฌ n < k * k ) : sqrt n - k < sqrt n + 2 - k :=
( tsub_lt_tsub_iff_right <| le_sqrt . 2 : โ {a b : Prop }, (a โ b b โ a <| le_of_not_gt h ). 2 : โ {a b : Prop }, (a โ b b โ a <| Nat.lt_add_of_pos_right : โ {n k : โ }, 0 < k n < n + k ( by decide )
#align nat.min_fac_lemma Nat.minFac_lemma
/-- If `n < k * k`, then `minFacAux n k = n`, if `k | n`, then `minFacAux n k = k`.
Otherwise, `minFacAux n k = minFacAux n (k+2)` using well-founded recursion.
If `n` is odd and `1 < n`, then then `minFacAux n 3` is the smallest prime factor of `n`. -/
def minFacAux ( n : โ ) : โ โ โ
| k =>
if h : n < k * k then n
else
if k โฃ n then k
else
have := minFac_lemma n k h
minFacAux n ( k + 2 )
termination_by _ n k => sqrt n + 2 - k
#align nat.min_fac_aux Nat.minFacAux
/-- Returns the smallest prime factor of `n โ 1`. -/
def minFac ( n : โ ) : โ :=
if 2 โฃ n then 2 else minFacAux n 3
#align nat.min_fac Nat.minFac
@[ simp ]
theorem minFac_zero : minFac 0 = 2 :=
rfl : โ {ฮฑ : Sort ?u.30139} {a : ฮฑ }, a = a
#align nat.min_fac_zero Nat.minFac_zero
@[ simp ]
theorem minFac_one : minFac 1 = 1 :=
rfl : โ {ฮฑ : Sort ?u.30187} {a : ฮฑ }, a = a
#align nat.min_fac_one Nat.minFac_one
theorem minFac_eq ( n : โ ) : minFac n = if 2 โฃ n then 2 else minFacAux n 3 := rfl : โ {ฮฑ : Sort ?u.30279} {a : ฮฑ }, a = a
#align nat.min_fac_eq Nat.minFac_eq
private def minFacProp ( n k : โ ) :=
2 โค k โง k โฃ n โง โ m , 2 โค m โ m โฃ n โ k โค m
theorem minFacAux_has_prop : โ {n : โ }, 2 โค n โ (k i : โ ), k = 2 * i + 3 (โ (m : โ ), 2 โค m m โฃ n k โค m ) โ Nat.minFacProp n (minFacAux n k minFacAux_has_prop { n : โ } ( n2 : 2 โค n ) :
โ k i , k = 2 * i + 3 โ (โ m , 2 โค m โ m โฃ n โ k โค m ) โ minFacProp n ( minFacAux n k )
| k => fun i e a => by
rw [ minFacAux Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 )] Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 )
by_cases h : n < k * k pos Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 )neg Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 ) Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 )<;> pos Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 )neg Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 ) Nat.minFacProp n
(if h : n < xโ * xโ n
else
if xโ โฃ n xโ
else
let_fun this := (_ : sqrt n - xโ < sqrt n + 2 - xโ ;
minFacAux n (xโ + 2 )simp [ h ] neg Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 )
ยท pos Nat.minFacProp n n
neg Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 )have pp : Prime n :=
prime_def_le_sqrt . 2 : โ {a b : Prop }, (a โ b b โ a
โจ n2 , fun m m2 l d => not_lt_of_ge : โ {ฮฑ : Type ?u.32837} [inst : Preorder ฮฑ a b : ฮฑ }, a โฅ b ยฌ a < b l <| lt_of_lt_of_le : โ {ฮฑ : Type ?u.32893} [inst : Preorder ฮฑ a b c : ฮฑ }, a < b b โค c a < c ( sqrt_lt . 2 : โ {a b : Prop }, (a โ b b โ a h ) ( a m m2 d )โฉ
exact โจ n2 , dvd_rfl : โ {ฮฑ : Type ?u.32957} [inst : Monoid ฮฑ a : ฮฑ }, a โฃ a , fun m m2 d => le_of_eq : โ {ฮฑ : Type ?u.32997} [inst : Preorder ฮฑ a b : ฮฑ }, a = b a โค b (( dvd_prime_two_le pp m2 ). 1 : โ {a b : Prop }, (a โ b a โ b d ). symm : โ {ฮฑ : Sort ?u.33031} {a b : ฮฑ }, a = b b = a symm โฉ
have k2 : 2 โค k := neg Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 )by
subst e
apply Nat.le_add_left : โ (n m : โ ), n โค m + n
by_cases dk : k โฃ n pos Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 )neg Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 ) neg Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 )<;> pos Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 )neg Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 ) neg Nat.minFacProp n (if xโ โฃ n xโ else minFacAux n (xโ + 2 )simp [ dk ]
ยท pos Nat.minFacProp n xโ
neg exact โจ k2 , dk , a โฉ
ยท refine'
have := minFac_lemma n k h
minFacAux_has_prop : โ {n : โ }, 2 โค n โ (k i : โ ), k = 2 * i + 3 (โ (m : โ ), 2 โค m m โฃ n k โค m ) โ Nat.minFacProp n (minFacAux n k minFacAux_has_prop n2 ( k + 2 ) ( i + 1 ) ( by simp [ e , left_distrib ] ) fun m