How to configure SSH keys for different GitHub accounts on the same pc

Recently I fought - and at the end succeded - to configure two different set of SSH keys for different GitHub accounts on the same computer.
I’m writing it down the procedure, so that I won’t have to repeat this fight again.

Create two different SSH keys, and add both on GitHub.
The documentation on GitHub explains the details.
SSH config
The SSH key config file is usually located at ~/.ssh/config. Open it with your editor of choice and paste the text below.
Note how HostName is in both case github.com, but Host, and IdentityFile are different.

Host github.com
  HostName github.com
  User git
  AddKeysToAgent yes
  UseKeychain yes
  IdentitiesOnly yes
  IdentityFile ~/.ssh/id_ed25519

Host github.com-b
  HostName github.com
  User git
  AddKeysToAgent yes
  UseKeychain yes
  IdentitiesOnly yes
  IdentityFile ~/.ssh/id_ed25519_b

Finally, for each repository for which you want to use the key id_ed25519_b, open its .git/config file and configure the remote, so that it matches the host precedently set in the SSH config file.
This last step is not needed when you clone directly from git@github.com-b:<username>/<repo>.git.

[remote "origin"]
  url = git@github.com-b:<username>/<repo>.git