Draft: More proofs for the add function#9

clarus merged 2 commits intomainformal-land/coq-of-python:mainfrom

guillaume-claret@verify-addformal-land/coq-of-python:guillaume-claret@verify-addCopy head branch name to clipboard