Formerly deferred structural inputs

Both structural inputs formerly deferred by the magnitude-conjecture formalization campaign are now proved. This compatibility module imports their completed development without adding any axiom boundary.