Hopf problem: threefold · special periods 9

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.SpecialPeriods.EllipticAttachingMeridians.norm_one_sub_coe_interval_mo1973_23381 (s : ↑unitInterval) : ‖↑(1 - ↑s)‖ = 1 - ↑s