MarkusKL

Encryption has shared secret as first component: https://github.com/SSProve/ssprove/blob/b5b89d660567d676b5c25533dae58dd397414593/theories/Crypt/examples/ElGamal.v#L159 Decryption computes inverse on the second component (not shared secret): https://github.com/SSProve/ssprove/blob/b5b89d660567d676b5c25533dae58dd397414593/theories/Crypt/examples/ElGamal.v#L166

Porting which parts, the experimental_reals code? And to this [this](https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.Rseries.html#) and related theories? An important and hard result that we rely on is the swapping of abs. convergent sums/integrals. Is...

I am happy to make the necessary updates to SSProve, and I think that it would be great to get rid of the admitted lemmas this way. I also know...

This header introduces the extra `fmap` definitions: https://github.com/SSProve/ssprove/blob/main/theories/Crypt/package/fmap_extra.v#L13 They are defined in `Prop` to not require `EqDec` on the values of the map. My work on nominals is to be...

The issues is still relevant since SSProve is still based on extructures.

I created a draft PR here to track the progress of replacing the inductively defined choice_type with the extensible set of countType. https://github.com/MarkusKL/ssprove/pull/1

This PR is ready for review. - I would suggest merging this into a new branch e.g. `towards-nominals`, so that all breaking changes can be introduced at once. - Does...

Thanks. I changed the base branch. Feel free to merge. I will make a thorough update of the documentation after more changes.