Generalized El-Gamal cipher implemented in Idris
#1Data.Encrypt.prf
I've no idea how to build darcs for win64 but that proof in Data.Encrypt is:
prf : {auto smaller : LTE 1 n} -> S (n - 1) = n
prf {smaller} {n = Z} = absurd smaller
prf {n = S k} = cong $ minusZeroRight k