EasyCrypt still feels better for crypto proofs; Coq wins when you want executable artifacts.

The bit about unwinding lemmas is the part people tend to skim past, but it matters because it turns a global security claim into local per-step checks. Instead of proving "the whole run never leaks", you prove that one instruction at a time cant make two attacker-indistinguishable states diverge in a visible way, which is a much more tractable shape for proof assistants. That same trick is what makes the later constant-time stuff feel less mystical, its really just noninterference against a leakage model where branch conditions and memory addresses count as observations.

Certification is the annoying bit (proof scripts are one thing, audit trails are another).