Step
*
1
of Lemma
grp_car_inc
.....subterm..... T:t
1:n
1. x : |(<ℤ+>↓hgrp)|
⊢ x ∈ ℕ
BY
{ (Reduce 1 THENM D 1 THENM Eval ``grp_leq`` 2 THENM RW bool_to_propC 2 THEN Auto) }
Latex:
Latex:
.....subterm..... T:t
1:n
1. x : |(<\mBbbZ{}+>\mdownarrow{}hgrp)|
\mvdash{} x \mmember{} \mBbbN{}
By
Latex:
(Reduce 1 THENM D 1 THENM Eval ``grp\_leq`` 2 THENM RW bool\_to\_propC 2 THEN Auto)
Home
Index