Skip to content

Instantly share code, notes, and snippets.

@esmooov

esmooov/gist:c224c2c88b8807ec685e

Created May 1, 2014 00:16
Show Gist options
  • Save esmooov/c224c2c88b8807ec685e to your computer and use it in GitHub Desktop.
Save esmooov/c224c2c88b8807ec685e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
---------- Assumptions: ---------- │~
k : Nat │~
m : Nat │~
---------- Goal: ---------- │~
{hole2} : inverseA (replace (plusCommutative m (S k)) │~
(replace (plusSuccRightSucc m k) (mkMD (S m) k))) = │~
mkMD (S k) m
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment