'BlockGaussianStep.kp_sum_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.completing_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.block_psd_iff_schur' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.schur_le_restricted' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.core_posDef' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.core_quadratic_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.coupling_step_iff_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.ratio_window_iff_quadratic' depends on axioms: [propext, Classical.choice, Quot.sound]
