0 | ||| Additional properties/lemmata of Nats
 1 | module Data.Nat.Properties
 2 |
 3 | import Data.Nat
 4 | import Syntax.PreorderReasoning
 5 |
 6 | %default total
 7 |
 8 | export
 9 | unfoldDouble : {0 n : Nat} -> (2 * n) === (n + n)
10 | unfoldDouble = irrelevantEq $ cong (n +) (plusZeroRightNeutral _)
11 |
12 | export
13 | unfoldDoubleS : {0 n : Nat} -> (2 * S n) === (2 + 2 * n)
14 | unfoldDoubleS = irrelevantEq $ Calc $
15 |   |~ 2 * S n
16 |   ~~ S n + S n   ...( unfoldDouble {n = S n} )
17 |   ~~ 2 + (n + n) ...( sym (plusSuccRightSucc (S n) n) )
18 |   ~~ 2 + 2 * n   ...( cong (2 +) (sym unfoldDouble) )
19 |
20 | export
21 | multRightCancel : (a,b,r : Nat) -> (0 _ : NonZero r) -> a*r = b*r -> a = b
22 | multRightCancel a      b    0           r_nz ar_eq_br = void (absurd r_nz)
23 | multRightCancel 0      0    r@(S predr) r_nz ar_eq_br = Refl
24 | multRightCancel 0     (S b) r@(S predr) r_nz ar_eq_br impossible
25 | multRightCancel (S a)  0    r@(S predr) r_nz ar_eq_br impossible
26 | multRightCancel (S a) (S b) r@(S predr) r_nz ar_eq_br =
27 |   cong S $ multRightCancel a b r r_nz
28 |          $ plusLeftCancel r (a*r) (b*r) ar_eq_br
29 |