2014-01-20 21:15:46 -08:00
|
|
|
Set: pp::colors
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
Assumed: f
|
|
|
|
|
Assumed: g
|
|
|
|
|
Assumed: a
|
|
|
|
|
Assumed: fid
|
|
|
|
|
Assumed: gcnst
|
2014-02-01 18:27:14 -08:00
|
|
|
Proved: one_neq_0
|
2014-01-20 21:15:46 -08:00
|
|
|
a
|
2014-02-01 18:27:14 -08:00
|
|
|
fid a
|
2014-02-09 16:15:44 -08:00
|
|
|
(eqt_elim (trans (trans (congr1 (congr2 neq (gcnst a)) 0) neq_to_not_eq)
|
2014-02-01 18:27:14 -08:00
|
|
|
(trans (congr2 not (neq_elim one_neq_0)) not_false)))
|
