Step
*
2
of Lemma
mul-imin
1. n : ℕ
2. a : ℤ
3. b : ℤ
4. ¬(a ≤ b)
5. (n * a) ≤ (n * b)
⊢ (n * b) = (n * a) ∈ ℤ
BY
{ (Assert ⌜(n * b) ≤ (n * a)⌝⋅ THEN EAuto 1) }
Latex:
Latex:
1.  n  :  \mBbbN{}
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  \mneg{}(a  \mleq{}  b)
5.  (n  *  a)  \mleq{}  (n  *  b)
\mvdash{}  (n  *  b)  =  (n  *  a)
By
Latex:
(Assert  \mkleeneopen{}(n  *  b)  \mleq{}  (n  *  a)\mkleeneclose{}\mcdot{}  THEN  EAuto  1)
Home
Index