ElGamal decryption incorrect

[MarkusKL]

It seems that the use of fst and snd are swapped in the ElGamal decryption algorithm in the examples. I would suggest adding a correctness game to AsymScheme.v and prove perfect correctness for the ElGamal scheme to make the correctness guarantee explicit.

I will attempt to make a PR with these changes in due time.

[MarkusKL]

Encryption has shared secret as first component:

ssprove/theories/Crypt/examples/ElGamal.v

Line 159 in b5b89d6

ret (fto (g^+y, (otf pk)^+y * (otf m)))

Decryption computes inverse on the second component (not shared secret):

ssprove/theories/Crypt/examples/ElGamal.v

Line 166 in b5b89d6

ret (fto ((fst (otf c)) * ((snd (otf c))^-(otf sk))))