@@ -0,0 +1,19 @@
1+module Data.Nat.Views
2+
3+||| View for expressing a number as a multiplication + a remainder
4+public export
5+data Divides : Integer -> (d : Integer) -> Type where
6+ DivByZero : Divides x 0
7+ DivBy : (prf : rem >= 0 && rem < d = True) ->
8+ Divides ((d * div) + rem) d
9+
10+||| Covering function for the `Divides` view
11+export
12+divides : (val : Integer) -> (d : Integer) -> Divides val d
13+divides val 0 = DivByZero
14+divides val d
15+ = let dividend = if d < 0 then -(val `div` abs d)
16+ else val `div` d
17+ remainder = val `mod` d in
18+ believe_me (DivBy {d} {div = dividend} {rem = remainder}
19+ (believe_me (Refl {x = True})))