A formal proof of $D^n / \partial D^n \cong S^n$