2014-01-29 22:21:18 +00:00
|
|
|
|
Set: pp::colors
|
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
|
Imported 'tactic'
|
|
|
|
|
|
Assumed: f
|
|
|
|
|
|
Assumed: Ax1
|
|
|
|
|
|
Assumed: Ax2
|
|
|
|
|
|
Proved: T1
|
2014-02-02 02:27:14 +00:00
|
|
|
|
theorem T1 (a : ℕ) : f (f a > 0) :=
|
|
|
|
|
|
eqt_elim (trans (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥)) not_false)
|
