Solution to borda#15

peritoflores wants to merge 2 commits intoCertora:masterCertora/tutorials-code:masterfrom

peritoflores:masterperitoflores/tutorials-code:masterCopy head branch name to clipboard