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