Fill in the sorry in `contiguous2_iff_contiguous3` in line 128 in #10. The proof is given below: <img width="940" height="710" alt="Image" src="https://github.com/user-attachments/assets/bc3f481a-4cf4-4838-ad7a-d7693612741c" />
Fill in the sorry in
contiguous2_iff_contiguous3in line 128 in #10. The proof is given below: