Step
*
1
2
of Lemma
mul_preserves_le
1. a : ℤ
2. b : ℤ
3. n : ℤ
4. n ≥ 0
5. a ≤ b
6. 0 = n ∈ ℤ
⊢ (n * a) ≤ (n * b)
BY
{ TACTIC:(RevHypSubst' (-1) 0 THEN Auto) }
Latex:
Latex:
1. a : \mBbbZ{}
2. b : \mBbbZ{}
3. n : \mBbbZ{}
4. n \mgeq{} 0
5. a \mleq{} b
6. 0 = n
\mvdash{} (n * a) \mleq{} (n * b)
By
Latex:
TACTIC:(RevHypSubst' (-1) 0 THEN Auto)
Home
Index