'FredholmSpace.rank_ker_comp_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FredholmSpace.every_integer_is_an_index' depends on axioms: [propext, Classical.choice, Quot.sound]