CoCalc Public Filestmp / a.leanOpen in with one click!
Author: William A. Stein
1
import data.rat.basic tactic
2
3
-- prove one and delete the other
4
5
theorem some_reciprocal_is_zero : x : , 1 / x = 0 :=
6
begin
7
sorry
8
end
9
10
theorem no_reciprocal_is_zero : ¬ ( x : , 1 / x = 0) :=
11
begin
12
sorry
13
end