Created
April 20, 2017 02:25
-
-
Save mjgpy3/00c64bfe3b7d131237b1e4ded020b50f to your computer and use it in GitHub Desktop.
Plus Commutes
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n | |
| myPlusCommutes Z Z = Refl | |
| myPlusCommutes Z (S k) = rewrite plusZeroRightNeutral (S k) in Refl | |
| myPlusCommutes (S k) Z = rewrite plusZeroRightNeutral (S k) in Refl | |
| myPlusCommutes (S k) (S j) = | |
| cong {f=S} (rewrite sym (plusSuccRightSucc k j) in (rewrite myPlusCommutes k j in (rewrite plusSuccRightSucc j k in Refl))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment