Mercurial > hg > Papers > 2015 > atton-thesis
view src/nat_add_sym_reasoning.agda @ 49:ba7f0b5454ab
Add description for DeltaM definition
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 15 Feb 2015 14:07:07 +0900 |
parents | c684abcc781b |
children |
line wrap: on
line source
open import Relation.Binary.PropositionalEquality open import nat open import nat_add open ≡-Reasoning module nat_add_sym_reasoning where addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m) addToRight O m = refl addToRight (S n) m = cong S (addToRight n m) addSym : (n m : Nat) -> n + m ≡ m + n addSym O O = refl addSym O (S m) = cong S (addSym O m) addSym (S n) O = cong S (addSym n O) addSym (S n) (S m) = begin (S n) + (S m) ≡⟨ refl ⟩ S (n + S m) ≡⟨ cong S (addSym n (S m)) ⟩ S ((S m) + n) ≡⟨ addToRight (S m) n ⟩ S (m + S n) ≡⟨ refl ⟩ (S m) + (S n) ∎