[GOAL]
a b : PosNum
⊢ Decidable ((fun x x_1 => x < x_1) a b)
[PROOFSTEP]
dsimp [LT.lt]
[GOAL]
a b : PosNum
⊢ Decidable (cmp a b = lt)
[PROOFSTEP]
infer_instance
[GOAL]
a b : PosNum
⊢ Decidable ((fun x x_1 => x ≤ x_1) a b)
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
a b : PosNum
⊢ Decidable ¬b < a
[PROOFSTEP]
infer_instance
[GOAL]
a b : Num
⊢ Decidable ((fun x x_1 => x < x_1) a b)
[PROOFSTEP]
dsimp [LT.lt]
[GOAL]
a b : Num
⊢ Decidable (cmp a b = lt)
[PROOFSTEP]
infer_instance
[GOAL]
a b : Num
⊢ Decidable ((fun x x_1 => x ≤ x_1) a b)
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
a b : Num
⊢ Decidable ¬b < a
[PROOFSTEP]
infer_instance
[GOAL]
a b : ZNum
⊢ Decidable ((fun x x_1 => x < x_1) a b)
[PROOFSTEP]
dsimp [LT.lt]
[GOAL]
a b : ZNum
⊢ Decidable (cmp a b = lt)
[PROOFSTEP]
infer_instance
[GOAL]
a b : ZNum
⊢ Decidable ((fun x x_1 => x ≤ x_1) a b)
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
a b : ZNum
⊢ Decidable ¬b < a
[PROOFSTEP]
infer_instance
