audit-session035-axioms.txt
5 declarations audited · 3 standard axioms only · updated 08-24-2026
Raw #print axioms transcript
'NguyenRH1.one_le_zeroMult' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exists_zero_avoiding_T' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exists_gapCircle_radius' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gentire_const' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.partialFraction_identity' depends on axioms: [propext, Classical.choice, Quot.sound]