Certified solutions for the three public-core declarations

The three declarations selected by comparator.json are the existing certified V7 exports imported above. No theorem is reproved or restated here.