2020-06-30 12:51:09 +03:00
|
|
|
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
|
|
|
plus_commutes_Z Z = Refl
|
|
|
|
plus_commutes_Z (S k)
|
|
|
|
= let rec = plus_commutes_Z k in
|
|
|
|
rewrite sym rec in Refl
|
|
|
|
|
|
|
|
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
|
|
|
|
plus_commutes_S k Z = Refl
|
|
|
|
plus_commutes_S k (S j)
|
|
|
|
= rewrite plus_commutes_S k j in Refl
|
|
|
|
|
|
|
|
total
|
|
|
|
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
|
|
|
plus_commutes Z m = plus_commutes_Z m
|
2021-01-16 10:03:45 +03:00
|
|
|
plus_commutes (S k) m
|
2020-06-30 12:51:09 +03:00
|
|
|
= rewrite plus_commutes k m in
|
|
|
|
plus_commutes_S k m
|