18 lines
296 B
Text
18 lines
296 B
Text
import data.nat
|
|
open nat
|
|
|
|
constant P : nat → Prop
|
|
|
|
example (Hex : ∃ n, P n) : true :=
|
|
obtain n Hn, from Hex,
|
|
begin
|
|
note Hn2 := Hn,
|
|
exact trivial
|
|
end
|
|
|
|
example (Hex : ∃ n, P n) : true :=
|
|
obtain n Hn, from Hex,
|
|
begin
|
|
have H : n ≥ 0, from sorry,
|
|
exact trivial
|
|
end
|