'RiemannRoch.finrank_degreeLT' depends on axioms: [propext, Classical.choice, Quot.sound]
'RiemannRoch.ell_P1' depends on axioms: [propext, Classical.choice, Quot.sound]