Step
*
2
1
of Lemma
pdivisor_bound
1. a : ℕ
2. b : ℕ+
3. a < b
4. a | b
5. b | a
6. a ~ b
⊢ False
BY
{ (FLemma `assoced_nelim` [-1] THEN Auto) }
Latex:
Latex:
1. a : \mBbbN{}
2. b : \mBbbN{}\msupplus{}
3. a < b
4. a | b
5. b | a
6. a \msim{} b
\mvdash{} False
By
Latex:
(FLemma `assoced\_nelim` [-1] THEN Auto)
Home
Index