'StrongCouplingOneSided.four_mul_le_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.area_le_strip' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.strip_term_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.strip_coeff_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.tube_coeff_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.tube_part_nonpos' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.h_main_term' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.h_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'StrongCouplingOneSided.h_neg_on_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
