Step
*
of Lemma
nat_inc
ℕ ⊆r |(<ℤ+>↓hgrp)|
BY
{ (Computation THEN Reduce 0 THEN RepUR ``int_add_grp grp_leq`` 0 THEN Auto) }
Latex:
Latex:
\mBbbN{} \msubseteq{}r |(<\mBbbZ{}+>\mdownarrow{}hgrp)|
By
Latex:
(Computation THEN Reduce 0 THEN RepUR ``int\_add\_grp grp\_leq`` 0 THEN Auto)
Home
Index