(* smallest factor *)
definition smallest_factor : nat → nat ≝
-λn:nat. if_then_else ? (leb n 1) n
- (min n 2 (λm.(eqb (n \mod m) O))).
+λn:nat. if leb n 1 then n else min n 2 (λm.(eqb (n \mod m) O)).
theorem smallest_factor_to_min : ∀n. 1 < n →
smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
min upper_bound (S previous_prime) primeb].
lemma nth_primeS: ∀n.nth_prime (S n) =
- let previous_prime ≝ nth_prime n in
+ (let previous_prime ≝ nth_prime n in
let upper_bound ≝ S previous_prime! in
- min upper_bound (S previous_prime) primeb.
+ min upper_bound (S previous_prime) primeb).
// qed.
(* it works *)