N (axiom)
NAxiomsSig.pred_0 [in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion [in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion_succ [in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion_wd [in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion_0 [in Coq.Numbers.Natural.Abstract.NAxioms]
NType.add [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.compare [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.div [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.div_eucl [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.eq_bool [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.gcd [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.modulo [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.mul [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.of_N [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.one [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.power_pos [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.pred [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_add [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_compare [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_div [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_div_eucl [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_eq_bool [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_gcd [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_modulo [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_mul [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_of_N [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pos [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_power_pos [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pred [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pred0 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sqrt [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_square [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sub [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sub0 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_succ [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_0 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_1 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.sqrt [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.square [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.sub [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.succ [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.t [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.to_Z [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.zero [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType_ZType.spec_Zabs_N [in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.spec_Z_of_N [in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.Zabs_N [in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.Z_of_N [in Coq.Numbers.Rational.BigQ.QMake]
NZAxiomsSig.NZ [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZadd [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZadd_succ_l [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZadd_0_l [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZeq [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZeq_equiv [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZinduction [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZmul [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZmul_succ_l [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZmul_0_l [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZpred [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZpred_succ [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsub [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsub_succ_r [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsub_0_r [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsucc [in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZ0 [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZle [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt_eq_cases [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt_irrefl [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt_succ_r [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmax [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmax_l [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmax_r [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmin [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmin_l [in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmin_r [in Coq.Numbers.NatInt.NZAxioms]