Why idris2 can't proof that div 1 2 < 1 = True?

Question

When I write:

div_1_2_lower_than_1 : div (S Z) 2 < (S Z) = True
div_1_2_lower_than_1 = Refl

I get error:

While processing right hand side of div_1_2_lower_than_1. Can't solve constraint
between: True and compare (1 `div` 2) 1 == LT.

Meanwhile when I write:

minus_1_2_lower_than_1 : minus (S Z) 2 < (S Z) = True
minus_1_2_lower_than_1 = Refl

Everything is fine. Why?

Updated:

I used Data.Nat and natDiv for some reason fundamentally not validated.

div_1_2_eq_0 : div (S Z) (S (S Z)) = 0
div_1_2_eq_0 = Refl

Error:

While processing right hand side of div_1_2_eq_0. Can't solve constraint between: 0 and divNat 1 2.

Answer 1

I think this is right. The implementation of div isn't exported so the type checker can't reduce it

export partial
divNat : Nat -> Nat -> Nat

public export
Integral Nat where
  div = divNat

You can try using divNatNZ instead, which is public exported, though for some reason it expects the non-zero proof explicitly.