Step
*
of Lemma
mul_nat_plus
∀[a,b:ℕ
+
].  (a * b ∈ ℕ
+
)
BY
{ Auto }
Latex:
Latex:
\mforall{}[a,b:\mBbbN{}\msupplus{}].    (a  *  b  \mmember{}  \mBbbN{}\msupplus{})
By
Latex:
Auto
Home
Index