# principia-ym-boundary-mixed-derivative-2026-10-29: `#print axioms` output, checked 2026-10-29 (rc=0, no sorry). All lines are subsets of propext / Classical.choice / Quot.sound.

## StrongCouplingOneSidedTerm.lean
'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]