'lemma5_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
'lemma5_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'lemma5_abs_le' depends on axioms: [propext, Classical.choice, Quot.sound]
