%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 12 07:13:47 PM UTC 2026 % Result : Theorem 6.23s 6.56s % Output : Proof 6.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.15/0.34 % Computer : n019.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Mon May 11 14:06:30 EDT 2026 % 0.15/0.34 % CPUTime : % 6.23/6.56 % SZS status Theorem % 6.23/6.56 % SZS output start Proof % 6.23/6.56 % 6.23/6.56 =============================================================== % 6.23/6.56 TPTP Problem: _HAMMER_GOAL (conjecture with 1727 axiom(s)) % 6.23/6.56 Axioms: [_HAMMER_COQ_TRUE,_HAMMER_COQ_FALSE,_HAMMER_COQ_TYPE_TYPE,$_case_Coq.Init.Datatypes.nat$32068,$_case_Coq.Init.Datatypes.nat$32090,$_case_Coq.Init.Datatypes.prod$16639,$_case_Coq.Init.Datatypes.prod$16654,$_case_Coq.Init.Datatypes.prod$964,$_case_Coq.Numbers.BinNums.Z$32085,$_def_$_let_11_subst_l_14524,$_def_$_let_1_s_19231,$_def_$_let_2_s_19729,$_def_Coq.Init.Datatypes.CompOpp,$_def_Coq.Init.Datatypes.andb,$_def_Coq.Init.Datatypes.nat_rec,$_def_Coq.Init.Datatypes.nat_rect,$_def_Coq.Init.Datatypes.negb,$_def_Coq.Init.Datatypes.orb,$_def_Coq.Init.Datatypes.snd,$_def_Coq.Init.Datatypes.xorb,$_def_Coq.Init.Nat.add,$_def_Coq.Init.Nat.compare,$_def_Coq.Init.Nat.max,$_def_Coq.Init.Nat.mul,$_def_Coq.Init.Nat.sub,$_def_Coq.Init.Peano.lt,$_def_Coq.Init.Wf.well_founded,$_def_Coq.Init.Wf.well_founded_induction_type,$_def_Coq.Logic.Decidable.decidable,$_def_Coq.NArith.BinNat.N.le,$_def_Coq.NArith.BinNat.N.lt,$_def_Coq.NArith.BinNatDef.N.add,$_def_Coq.NArith.BinNatDef.N.compare,$_def_Coq.NArith.BinNatDef.N.min,$_def_Coq.NArith.BinNatDef.N.mul,$_def_Coq.NArith.BinNatDef.N.of_nat,$_def_Coq.NArith.BinNatDef.N.sub,$_def_Coq.NArith.BinNatDef.N.succ,$_def_Coq.NArith.BinNatDef.N.testbit,$_def_Coq.NArith.BinNatDef.N.to_nat,$_def_Coq.PArith.BinPos.Pos.le,$_def_Coq.PArith.BinPos.Pos.lt,$_def_Coq.PArith.BinPosDef.Pos.add,$_def_Coq.PArith.BinPosDef.Pos.compare,$_def_Coq.PArith.BinPosDef.Pos.iter,$_def_Coq.PArith.BinPosDef.Pos.mul,$_def_Coq.PArith.BinPosDef.Pos.pred_N,$_def_Coq.PArith.BinPosDef.Pos.pred_double,$_def_Coq.PArith.BinPosDef.Pos.sqrt,$_def_Coq.PArith.BinPosDef.Pos.sub,$_def_Coq.PArith.BinPosDef.Pos.succ,$_def_Coq.PArith.BinPosDef.Pos.testbit,$_def_Coq.PArith.BinPosDef.Pos.to_nat,$_def_Coq.QArith.QArith_base.Qden,$_def_Coq.QArith.QArith_base.Qle,$_def_Coq.QArith.QArith_base.Qnum,$_def_Coq.Reals.Rdefinitions.IZR,$_def_Coq.Reals.Rdefinitions.Rle,$_def_Coq.Reals.Rpow_def.pow,$_def_Coq.Relations.Relation_Definitions.relation,$_def_Coq.ZArith.BinInt.Z.Odd,$_def_Coq.ZArith.BinInt.Z.b2z,$_def_Coq.ZArith.BinInt.Z.divide,$_def_Coq.ZArith.BinInt.Z.eqf,$_def_Coq.ZArith.BinInt.Z.ge,$_def_Coq.ZArith.BinInt.Z.gt,$_def_Coq.ZArith.BinInt.Z.lcm,$_def_Coq.ZArith.BinInt.Z.le,$_def_Coq.ZArith.BinInt.Z.lnot,$_def_Coq.ZArith.BinInt.Z.log2_up,$_def_Coq.ZArith.BinInt.Z.lt,$_def_Coq.ZArith.BinInt.Z.ones,$_def_Coq.ZArith.BinInt.Z.sqrt_up,$_def_Coq.ZArith.BinInt.Zne,$_def_Coq.ZArith.BinIntDef.Z.abs,$_def_Coq.ZArith.BinIntDef.Z.abs_N,$_def_Coq.ZArith.BinIntDef.Z.abs_nat,$_def_Coq.ZArith.BinIntDef.Z.add,$_def_Coq.ZArith.BinIntDef.Z.compare,$_def_Coq.ZArith.BinIntDef.Z.div,$_def_Coq.ZArith.BinIntDef.Z.div2,$_def_Coq.ZArith.BinIntDef.Z.eqb,$_def_Coq.ZArith.BinIntDef.Z.gcd,$_def_Coq.ZArith.BinIntDef.Z.leb,$_def_Coq.ZArith.BinIntDef.Z.log2,$_def_Coq.ZArith.BinIntDef.Z.ltb,$_def_Coq.ZArith.BinIntDef.Z.max,$_def_Coq.ZArith.BinIntDef.Z.min,$_def_Coq.ZArith.BinIntDef.Z.modulo,$_def_Coq.ZArith.BinIntDef.Z.mul,$_def_Coq.ZArith.BinIntDef.Z.odd,$_def_Coq.ZArith.BinIntDef.Z.of_N,$_def_Coq.ZArith.BinIntDef.Z.of_nat,$_def_Coq.ZArith.BinIntDef.Z.opp,$_def_Coq.ZArith.BinIntDef.Z.pos_sub,$_def_Coq.ZArith.BinIntDef.Z.pow,$_def_Coq.ZArith.BinIntDef.Z.pow_pos,$_def_Coq.ZArith.BinIntDef.Z.pred,$_def_Coq.ZArith.BinIntDef.Z.quot,$_def_Coq.ZArith.BinIntDef.Z.quotrem,$_def_Coq.ZArith.BinIntDef.Z.rem,$_def_Coq.ZArith.BinIntDef.Z.sgn,$_def_Coq.ZArith.BinIntDef.Z.shiftl,$_def_Coq.ZArith.BinIntDef.Z.shiftr,$_def_Coq.ZArith.BinIntDef.Z.sqrt,$_def_Coq.ZArith.BinIntDef.Z.sqrtrem,$_def_Coq.ZArith.BinIntDef.Z.sub,$_def_Coq.ZArith.BinIntDef.Z.succ,$_def_Coq.ZArith.BinIntDef.Z.testbit,$_def_Coq.ZArith.BinIntDef.Z.to_N,$_def_Coq.ZArith.BinIntDef.Z.to_nat,$_def_Coq.ZArith.BinIntDef.Z.to_pos,$_def_Coq.ZArith.ZArith_dec.Z_zerop,$_def_Coq.ZArith.Zbool.Zeq_bool,$_def_Coq.ZArith.Zdiv.Remainder,$_def_Coq.ZArith.Zeven.Zodd,$_def_Coq.ZArith.Znumtheory.rel_prime,$_def_Coq.ZArith.Zpower.Zdiv_rest_proofs_rect,$_def_Coq.ZArith.Zpower.Zpower_nat,$_def_Coq.ZArith.Zpower.two_p,$_def_Coq.ZArith.Zpower.two_power_pos,$_def_Coq.setoid_ring.Ring_polynom.Peq,$_def_Coq.setoid_ring.Ring_polynom.mk_monpol_list,$_def_Coq.setoid_ring.Ring_polynom.norm_subst,$_def_Coq.setoid_ring.Ring_tac.ring_subst_niter,$_discrim_Coq.Init.Datatypes.Eq$Coq.Init.Datatypes.Lt,$_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S,$_discrim_Coq.Init.Datatypes.nil$Coq.Init.Datatypes.cons,$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false,$_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right,$_discrim_Coq.Numbers.BinNums.N0$Coq.Numbers.BinNums.Npos,$_discrim_Coq.Numbers.BinNums.Z0$Coq.Numbers.BinNums.Zpos,$_discrim_Coq.Numbers.BinNums.xI$Coq.Numbers.BinNums.xO,$_discrim_Coq.PArith.BinPosDef.Pos.IsNul$Coq.PArith.BinPosDef.Pos.IsPos,$_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos,$_discrim_Coq.Structures.OrdersTac.OEQ$Coq.Structures.OrdersTac.OLT,$_discrim_Coq.setoid_ring.Ring_polynom.PEO$Coq.setoid_ring.Ring_polynom.PEI,$_discrim_Coq.setoid_ring.Ring_polynom.Pc$Coq.setoid_ring.Ring_polynom.Pinj,$_discrim_Coq.setoid_ring.Ring_polynom.mon0$Coq.setoid_ring.Ring_polynom.zmon,$_fix_413_1_add_carry,$_inj_Coq.Init.Datatypes.S,$_inj_Coq.Init.Datatypes.cons,$_inj_Coq.Init.Datatypes.nil,$_inj_Coq.Init.Datatypes.pair,$_inj_Coq.Init.Specif.exist,$_inj_Coq.Init.Specif.left,$_inj_Coq.Init.Specif.right,$_inj_Coq.Numbers.BinNums.Npos,$_inj_Coq.Numbers.BinNums.Zneg,$_inj_Coq.Numbers.BinNums.Zpos,$_inj_Coq.Numbers.BinNums.xI,$_inj_Coq.Numbers.BinNums.xO,$_inj_Coq.PArith.BinPosDef.Pos.IsPos,$_inj_Coq.QArith.QArith_base.Qmake,$_inj_Coq.Reals.Rfunctions.ZintNeg,$_inj_Coq.Reals.Rfunctions.ZintNull,$_inj_Coq.Reals.Rfunctions.ZintPos,$_inj_Coq.ZArith.Znumtheory.Euclid_intro,$_inj_Coq.ZArith.Zpower.Zdiv_rest_proof,$_inj_Coq.setoid_ring.Ring_polynom.PEI,$_inj_Coq.setoid_ring.Ring_polynom.PEO,$_inj_Coq.setoid_ring.Ring_polynom.PEX,$_inj_Coq.setoid_ring.Ring_polynom.PEadd,$_inj_Coq.setoid_ring.Ring_polynom.PEc,$_inj_Coq.setoid_ring.Ring_polynom.PEmul,$_inj_Coq.setoid_ring.Ring_polynom.PEopp,$_inj_Coq.setoid_ring.Ring_polynom.PEpow,$_inj_Coq.setoid_ring.Ring_polynom.PEsub,$_inj_Coq.setoid_ring.Ring_polynom.PX,$_inj_Coq.setoid_ring.Ring_polynom.Pc,$_inj_Coq.setoid_ring.Ring_polynom.Pinj,$_inj_Coq.setoid_ring.Ring_polynom.vmon,$_inj_Coq.setoid_ring.Ring_polynom.zmon,$_inversion_Coq.Init.Datatypes.BoolSpec,$_inversion_Coq.Init.Datatypes.CompareSpec,$_inversion_Coq.Init.Datatypes.bool,$_inversion_Coq.Init.Datatypes.comparison,$_inversion_Coq.Init.Datatypes.list,$_inversion_Coq.Init.Datatypes.nat,$_inversion_Coq.Init.Datatypes.prod,$_inversion_Coq.Init.Datatypes.unit,$_inversion_Coq.Init.Peano.le,$_inversion_Coq.Init.Specif.sig,$_inversion_Coq.Init.Specif.sumbool,$_inversion_Coq.Numbers.BinNums.N,$_inversion_Coq.Numbers.BinNums.Z,$_inversion_Coq.Numbers.BinNums.positive,$_inversion_Coq.PArith.BinPos.Pos.SqrtSpec,$_inversion_Coq.PArith.BinPosDef.Pos.mask,$_inversion_Coq.QArith.QArith_base.Q,$_inversion_Coq.Reals.Rfunctions.Z_spec,$_inversion_Coq.Structures.OrdersTac.ord,$_inversion_Coq.ZArith.Znumtheory.Bezout,$_inversion_Coq.ZArith.Znumtheory.Euclid,$_inversion_Coq.ZArith.Znumtheory.Zis_gcd,$_inversion_Coq.ZArith.Znumtheory.prime,$_inversion_Coq.ZArith.Zpower.Zdiv_rest_proofs,$_inversion_Coq.setoid_ring.Ring_polynom.Mon,$_inversion_Coq.setoid_ring.Ring_polynom.PExpr,$_inversion_Coq.setoid_ring.Ring_polynom.Pol,$_lam_14596,$_lam_18637,$_lam_18639,$_lam_259,$_lam_300,$_lam_59478,$_lam_68508,$_prop_13363,$_prop_19713,$_prop_34425,$_prop_34426,$_prop_35229,$_type_117,$_type_12,$_type_13186,$_type_13189,$_type_13192,$_type_13209,$_type_13214,$_type_13227,$_type_13229,$_type_13234,$_type_13315,$_type_13335,$_type_13340,$_type_13342,$_type_13361,$_type_13636,$_type_13657,$_type_13849,$_type_13869,$_type_13871,$_type_13874,$_type_13885,$_type_14048,$_type_14243,$_type_14254,$_type_14503,$_type_14506,$_type_14511,$_type_14728,$_type_14746,$_type_14906,$_type_16386,$_type_16391,$_type_16412,$_type_16414,$_type_16422,$_type_16816,$_type_16853,$_type_18641,$_type_18835,$_type_18872,$_type_18888,$_type_18949,$_type_18953,$_type_18982,$_type_18997,$_type_19090,$_type_19157,$_type_19160,$_type_19197,$_type_19204,$_type_19220,$_type_19222,$_type_19295,$_type_19298,$_type_19307,$_type_19311,$_type_19318,$_type_19321,$_type_19325,$_type_19459,$_type_19818,$_type_19822,$_type_21994,$_type_22003,$_type_22008,$_type_22011,$_type_245,$_type_25,$_type_286,$_type_30,$_type_31256,$_type_31347,$_type_31442,$_type_323,$_type_34421,$_type_34423,$_type_35232,$_type_376,$_type_392,$_type_399,$_type_401,$_type_410,$_type_443,$_type_45,$_type_471,$_type_515,$_type_525,$_type_57851,$_type_59295,$_type_59418,$_type_59522,$_type_59528,$_type_59550,$_type_59565,$_type_59575,$_type_59578,$_type_59635,$_type_59653,$_type_59662,$_type_60221,$_type_60500,$_type_60503,$_type_60511,$_type_60515,$_type_61,$_type_65103,$_type_68505,$_type_68531,$_type_68539,$_type_68555,$_type_68565,$_type_74,$_type_90,$_type_94,$_type_956,$_type_97,$_typeof_Coq.Init.Datatypes.CompOpp,$_typeof_Coq.Init.Datatypes.Eq,$_typeof_Coq.Init.Datatypes.Gt,$_typeof_Coq.Init.Datatypes.Lt,$_typeof_Coq.Init.Datatypes.O,$_typeof_Coq.Init.Datatypes.S,$_typeof_Coq.Init.Datatypes.andb,$_typeof_Coq.Init.Datatypes.bool,$_typeof_Coq.Init.Datatypes.comparison,$_typeof_Coq.Init.Datatypes.cons,$_typeof_Coq.Init.Datatypes.false,$_typeof_Coq.Init.Datatypes.list,$_typeof_Coq.Init.Datatypes.nat,$_typeof_Coq.Init.Datatypes.nat_rec,$_typeof_Coq.Init.Datatypes.nat_rect,$_typeof_Coq.Init.Datatypes.negb,$_typeof_Coq.Init.Datatypes.nil,$_typeof_Coq.Init.Datatypes.orb,$_typeof_Coq.Init.Datatypes.pair,$_typeof_Coq.Init.Datatypes.prod,$_typeof_Coq.Init.Datatypes.snd,$_typeof_Coq.Init.Datatypes.true,$_typeof_Coq.Init.Datatypes.tt,$_typeof_Coq.Init.Datatypes.unit,$_typeof_Coq.Init.Datatypes.xorb,$_typeof_Coq.Init.Nat.add,$_typeof_Coq.Init.Nat.compare,$_typeof_Coq.Init.Nat.max,$_typeof_Coq.Init.Nat.mul,$_typeof_Coq.Init.Nat.sub,$_typeof_Coq.Init.Peano.lt,$_typeof_Coq.Init.Specif.exist,$_typeof_Coq.Init.Specif.left,$_typeof_Coq.Init.Specif.right,$_typeof_Coq.Init.Specif.sig,$_typeof_Coq.Init.Specif.sumbool,$_typeof_Coq.Init.Wf.well_founded,$_typeof_Coq.Init.Wf.well_founded_induction_type,$_typeof_Coq.Logic.Decidable.decidable,$_typeof_Coq.NArith.BinNat.N.le,$_typeof_Coq.NArith.BinNat.N.lt,$_typeof_Coq.NArith.BinNatDef.N.add,$_typeof_Coq.NArith.BinNatDef.N.compare,$_typeof_Coq.NArith.BinNatDef.N.min,$_typeof_Coq.NArith.BinNatDef.N.mul,$_typeof_Coq.NArith.BinNatDef.N.of_nat,$_typeof_Coq.NArith.BinNatDef.N.sub,$_typeof_Coq.NArith.BinNatDef.N.succ,$_typeof_Coq.NArith.BinNatDef.N.testbit,$_typeof_Coq.NArith.BinNatDef.N.to_nat,$_typeof_Coq.Numbers.BinNums.N,$_typeof_Coq.Numbers.BinNums.N0,$_typeof_Coq.Numbers.BinNums.Npos,$_typeof_Coq.Numbers.BinNums.Z,$_typeof_Coq.Numbers.BinNums.Z0,$_typeof_Coq.Numbers.BinNums.Zneg,$_typeof_Coq.Numbers.BinNums.Zpos,$_typeof_Coq.Numbers.BinNums.positive,$_typeof_Coq.Numbers.BinNums.xH,$_typeof_Coq.Numbers.BinNums.xI,$_typeof_Coq.Numbers.BinNums.xO,$_typeof_Coq.PArith.BinPos.Pos.le,$_typeof_Coq.PArith.BinPos.Pos.lt,$_typeof_Coq.PArith.BinPosDef.Pos.add,$_typeof_Coq.PArith.BinPosDef.Pos.compare,$_typeof_Coq.PArith.BinPosDef.Pos.iter,$_typeof_Coq.PArith.BinPosDef.Pos.mask,$_typeof_Coq.PArith.BinPosDef.Pos.mul,$_typeof_Coq.PArith.BinPosDef.Pos.pred_N,$_typeof_Coq.PArith.BinPosDef.Pos.pred_double,$_typeof_Coq.PArith.BinPosDef.Pos.sqrt,$_typeof_Coq.PArith.BinPosDef.Pos.sub,$_typeof_Coq.PArith.BinPosDef.Pos.succ,$_typeof_Coq.PArith.BinPosDef.Pos.testbit,$_typeof_Coq.PArith.BinPosDef.Pos.to_nat,$_typeof_Coq.QArith.QArith_base.Q,$_typeof_Coq.QArith.QArith_base.Qden,$_typeof_Coq.QArith.QArith_base.Qle,$_typeof_Coq.QArith.QArith_base.Qnum,$_typeof_Coq.Reals.Rdefinitions.IZR,$_typeof_Coq.Reals.Rdefinitions.R,$_typeof_Coq.Reals.Rdefinitions.Rinv,$_typeof_Coq.Reals.Rdefinitions.Rle,$_typeof_Coq.Reals.Rdefinitions.Rlt,$_typeof_Coq.Reals.Rdefinitions.Rmult,$_typeof_Coq.Reals.Rfunctions.Z_spec,$_typeof_Coq.Reals.RiemannInt_SF.IZN_var,$_typeof_Coq.Reals.Rpow_def.pow,$_typeof_Coq.Relations.Relation_Definitions.relation,$_typeof_Coq.Structures.OrdersTac.ord,$_typeof_Coq.ZArith.BinInt.Z.Odd,$_typeof_Coq.ZArith.BinInt.Z.b2z,$_typeof_Coq.ZArith.BinInt.Z.divide,$_typeof_Coq.ZArith.BinInt.Z.eqf,$_typeof_Coq.ZArith.BinInt.Z.ge,$_typeof_Coq.ZArith.BinInt.Z.gt,$_typeof_Coq.ZArith.BinInt.Z.lcm,$_typeof_Coq.ZArith.BinInt.Z.le,$_typeof_Coq.ZArith.BinInt.Z.lnot,$_typeof_Coq.ZArith.BinInt.Z.log2_up,$_typeof_Coq.ZArith.BinInt.Z.lt,$_typeof_Coq.ZArith.BinInt.Z.ones,$_typeof_Coq.ZArith.BinInt.Z.sqrt_up,$_typeof_Coq.ZArith.BinInt.Zne,$_typeof_Coq.ZArith.BinIntDef.Z.abs,$_typeof_Coq.ZArith.BinIntDef.Z.abs_N,$_typeof_Coq.ZArith.BinIntDef.Z.abs_nat,$_typeof_Coq.ZArith.BinIntDef.Z.add,$_typeof_Coq.ZArith.BinIntDef.Z.compare,$_typeof_Coq.ZArith.BinIntDef.Z.div,$_typeof_Coq.ZArith.BinIntDef.Z.div2,$_typeof_Coq.ZArith.BinIntDef.Z.eqb,$_typeof_Coq.ZArith.BinIntDef.Z.gcd,$_typeof_Coq.ZArith.BinIntDef.Z.leb,$_typeof_Coq.ZArith.BinIntDef.Z.log2,$_typeof_Coq.ZArith.BinIntDef.Z.ltb,$_typeof_Coq.ZArith.BinIntDef.Z.max,$_typeof_Coq.ZArith.BinIntDef.Z.min,$_typeof_Coq.ZArith.BinIntDef.Z.modulo,$_typeof_Coq.ZArith.BinIntDef.Z.mul,$_typeof_Coq.ZArith.BinIntDef.Z.odd,$_typeof_Coq.ZArith.BinIntDef.Z.of_N,$_typeof_Coq.ZArith.BinIntDef.Z.of_nat,$_typeof_Coq.ZArith.BinIntDef.Z.opp,$_typeof_Coq.ZArith.BinIntDef.Z.pos_sub,$_typeof_Coq.ZArith.BinIntDef.Z.pow,$_typeof_Coq.ZArith.BinIntDef.Z.pow_pos,$_typeof_Coq.ZArith.BinIntDef.Z.pred,$_typeof_Coq.ZArith.BinIntDef.Z.quot,$_typeof_Coq.ZArith.BinIntDef.Z.quotrem,$_typeof_Coq.ZArith.BinIntDef.Z.rem,$_typeof_Coq.ZArith.BinIntDef.Z.sgn,$_typeof_Coq.ZArith.BinIntDef.Z.shiftl,$_typeof_Coq.ZArith.BinIntDef.Z.shiftr,$_typeof_Coq.ZArith.BinIntDef.Z.sqrt,$_typeof_Coq.ZArith.BinIntDef.Z.sqrtrem,$_typeof_Coq.ZArith.BinIntDef.Z.sub,$_typeof_Coq.ZArith.BinIntDef.Z.succ,$_typeof_Coq.ZArith.BinIntDef.Z.testbit,$_typeof_Coq.ZArith.BinIntDef.Z.to_N,$_typeof_Coq.ZArith.BinIntDef.Z.to_nat,$_typeof_Coq.ZArith.BinIntDef.Z.to_pos,$_typeof_Coq.ZArith.Wf_Z.Z_lt_rec,$_typeof_Coq.ZArith.Wf_Z.Z_of_nat_complete_inf,$_typeof_Coq.ZArith.Wf_Z.Z_of_nat_set,$_typeof_Coq.ZArith.Wf_Z.Zlt_lower_bound_rec,$_typeof_Coq.ZArith.Wf_Z.natlike_rec,$_typeof_Coq.ZArith.Wf_Z.natlike_rec2,$_typeof_Coq.ZArith.Wf_Z.natlike_rec3,$_typeof_Coq.ZArith.ZArith_dec.Z_zerop,$_typeof_Coq.ZArith.Zbool.Zeq_bool,$_typeof_Coq.ZArith.Zdiv.Remainder,$_typeof_Coq.ZArith.Zdiv.Zdiv_eucl_exist,$_typeof_Coq.ZArith.Zdiv.Zdiv_eucl_extended,$_typeof_Coq.ZArith.Zeven.Zodd,$_typeof_Coq.ZArith.Zmin.Zmin_le_prime_inf,$_typeof_Coq.ZArith.Znumtheory.Euclid,$_typeof_Coq.ZArith.Znumtheory.Euclid_intro,$_typeof_Coq.ZArith.Znumtheory.euclid_rec,$_typeof_Coq.ZArith.Znumtheory.rel_prime,$_typeof_Coq.ZArith.Zpower.Zdiv_rest_proof,$_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs,$_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs_rect,$_typeof_Coq.ZArith.Zpower.Zpower_nat,$_typeof_Coq.ZArith.Zpower.two_p,$_typeof_Coq.ZArith.Zpower.two_power_pos,$_typeof_Coq.setoid_ring.Ring_polynom.Mon,$_typeof_Coq.setoid_ring.Ring_polynom.PEX,$_typeof_Coq.setoid_ring.Ring_polynom.PEadd,$_typeof_Coq.setoid_ring.Ring_polynom.PEc,$_typeof_Coq.setoid_ring.Ring_polynom.PEmul,$_typeof_Coq.setoid_ring.Ring_polynom.PEsub,$_typeof_Coq.setoid_ring.Ring_polynom.PExpr,$_typeof_Coq.setoid_ring.Ring_polynom.Peq,$_typeof_Coq.setoid_ring.Ring_polynom.Pol,$_typeof_Coq.setoid_ring.Ring_polynom.mk_monpol_list,$_typeof_Coq.setoid_ring.Ring_polynom.norm_subst,$_typeof_Coq.setoid_ring.Ring_tac.ring_subst_niter,ArithCompl.sqr_0,ArithCompl.sqr_2,ArithCompl.sqr_ge,ArithCompl.sqr_le,ArithCompl.sqr_poss,ArithCompl.sqr_sub1,ArithCompl.sqr_sub2,ArithCompl.sqr_sub3,ArithCompl.sqr_sum2,ArithCompl.sqr_sum4,Coq.Init.Datatypes.nat_ind,Coq.Init.Specif.sumbool_ind,Coq.Logic.Decidable.dec_and,Coq.Logic.Decidable.dec_not_not,Coq.Logic.Decidable.not_and,Coq.PArith.BinPos.Pos.add_1_r,Coq.PArith.BinPos.Pos.add_comm,Coq.PArith.BinPos.Pos.iter_invariant,Coq.PArith.BinPos.Pos.iter_swap_gen,Coq.PArith.BinPos.Pos.sqrt_spec,Coq.PArith.BinPos.Pos.sqrtrem_spec,Coq.Reals.RIneq.IZN,Coq.Reals.RIneq.Rmult_0_l,Coq.Reals.RIneq.Rmult_0_r,Coq.Reals.RIneq.le_0_IZR,Coq.Reals.RIneq.le_IZR,Coq.Reals.RIneq.mult_IZR,Coq.Reals.Raxioms.Rmult_1_l,Coq.Reals.Rfunctions.Zpower_NR0,Coq.ZArith.BinInt.Pos2Z.is_nonneg,Coq.ZArith.BinInt.Z.A'A_left,Coq.ZArith.BinInt.Z.A'A_right,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.add_mod,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.add_mod_idemp_l,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.add_mod_idemp_r,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_1_r,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_add,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_add_l,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_div,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_exact,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_compat_l,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_lower_bound,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_mono,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_upper_bound,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_lt_upper_bound,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mod_unique,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul_cancel_l,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul_cancel_r,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul_le,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_pos,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_small,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_small_iff,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_str_pos,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_str_pos_iff,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_unique,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_unique_exact,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_1_r,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_add,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_divides,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_le,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_mod,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_mul,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_mul_r,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_small,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_small_iff,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_unique,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_div_le,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_distr_l,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_distr_r,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_idemp_l,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_idemp_r,Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_succ_div_gt,Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.div_mod,Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.div_wd,Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.mod_bound_pos,Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.mod_wd,Coq.ZArith.BinInt.Z.Private_NZDiv.add_mod,Coq.ZArith.BinInt.Z.Private_NZDiv.add_mod_idemp_l,Coq.ZArith.BinInt.Z.Private_NZDiv.add_mod_idemp_r,Coq.ZArith.BinInt.Z.Private_NZDiv.div_1_r,Coq.ZArith.BinInt.Z.Private_NZDiv.div_add,Coq.ZArith.BinInt.Z.Private_NZDiv.div_add_l,Coq.ZArith.BinInt.Z.Private_NZDiv.div_div,Coq.ZArith.BinInt.Z.Private_NZDiv.div_exact,Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_compat_l,Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_lower_bound,Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_mono,Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_upper_bound,Coq.ZArith.BinInt.Z.Private_NZDiv.div_lt_upper_bound,Coq.ZArith.BinInt.Z.Private_NZDiv.div_mod_unique,Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul,Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul_cancel_l,Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul_cancel_r,Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul_le,Coq.ZArith.BinInt.Z.Private_NZDiv.div_pos,Coq.ZArith.BinInt.Z.Private_NZDiv.div_small,Coq.ZArith.BinInt.Z.Private_NZDiv.div_small_iff,Coq.ZArith.BinInt.Z.Private_NZDiv.div_str_pos,Coq.ZArith.BinInt.Z.Private_NZDiv.div_str_pos_iff,Coq.ZArith.BinInt.Z.Private_NZDiv.div_unique,Coq.ZArith.BinInt.Z.Private_NZDiv.div_unique_exact,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_1_r,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_add,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_divides,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_le,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_mod,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_mul,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_mul_r,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_small,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_small_iff,Coq.ZArith.BinInt.Z.Private_NZDiv.mod_unique,Coq.ZArith.BinInt.Z.Private_NZDiv.mul_div_le,Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod,Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_distr_l,Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_distr_r,Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_idemp_l,Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_idemp_r,Coq.ZArith.BinInt.Z.Private_NZDiv.mul_succ_div_gt,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_le,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_lt,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_neq,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_refl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_sym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_trans,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_antisym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_eq,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_lt_trans,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_neq_lt,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_refl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_trans,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_eq,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_irrefl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_trans,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_eq,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_sym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_ge_lt,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_gt_le,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_neq_eq,Coq.ZArith.BinInt.Z.Private_Tac.eq_le,Coq.ZArith.BinInt.Z.Private_Tac.eq_sym,Coq.ZArith.BinInt.Z.Private_Tac.le_antisym,Coq.ZArith.BinInt.Z.Private_Tac.le_eq,Coq.ZArith.BinInt.Z.Private_Tac.le_neq_lt,Coq.ZArith.BinInt.Z.Private_Tac.le_trans,Coq.ZArith.BinInt.Z.Private_Tac.lt_irrefl,Coq.ZArith.BinInt.Z.Private_Tac.not_gt_le,Coq.ZArith.BinInt.Z.abs_0_iff,Coq.ZArith.BinInt.Z.abs_eq,Coq.ZArith.BinInt.Z.abs_neq,Coq.ZArith.BinInt.Z.abs_nonneg,Coq.ZArith.BinInt.Z.abs_sgn,Coq.ZArith.BinInt.Z.abs_spec,Coq.ZArith.BinInt.Z.add_0_l,Coq.ZArith.BinInt.Z.add_0_r,Coq.ZArith.BinInt.Z.add_1_l,Coq.ZArith.BinInt.Z.add_1_r,Coq.ZArith.BinInt.Z.add_assoc,Coq.ZArith.BinInt.Z.add_cancel_l,Coq.ZArith.BinInt.Z.add_cancel_r,Coq.ZArith.BinInt.Z.add_comm,Coq.ZArith.BinInt.Z.add_le_cases,Coq.ZArith.BinInt.Z.add_le_lt_mono,Coq.ZArith.BinInt.Z.add_le_mono,Coq.ZArith.BinInt.Z.add_le_mono_l,Coq.ZArith.BinInt.Z.add_le_mono_r,Coq.ZArith.BinInt.Z.add_lt_le_mono,Coq.ZArith.BinInt.Z.add_lt_mono,Coq.ZArith.BinInt.Z.add_lt_mono_l,Coq.ZArith.BinInt.Z.add_lt_mono_r,Coq.ZArith.BinInt.Z.add_neg_nonpos,Coq.ZArith.BinInt.Z.add_nonneg_cases,Coq.ZArith.BinInt.Z.add_nonneg_nonneg,Coq.ZArith.BinInt.Z.add_nonneg_pos,Coq.ZArith.BinInt.Z.add_nonpos_cases,Coq.ZArith.BinInt.Z.add_nonpos_neg,Coq.ZArith.BinInt.Z.add_nonpos_nonpos,Coq.ZArith.BinInt.Z.add_opp_r,Coq.ZArith.BinInt.Z.add_pos_nonneg,Coq.ZArith.BinInt.Z.add_pos_pos,Coq.ZArith.BinInt.Z.add_rem,Coq.ZArith.BinInt.Z.add_rem_idemp_l,Coq.ZArith.BinInt.Z.add_rem_idemp_r,Coq.ZArith.BinInt.Z.add_shuffle0,Coq.ZArith.BinInt.Z.add_simpl_r,Coq.ZArith.BinInt.Z.add_sqrt_le,Coq.ZArith.BinInt.Z.add_sqrt_up_le,Coq.ZArith.BinInt.Z.add_square_le,Coq.ZArith.BinInt.Z.add_sub_assoc,Coq.ZArith.BinInt.Z.add_sub_swap,Coq.ZArith.BinInt.Z.add_succ_l,Coq.ZArith.BinInt.Z.add_succ_r,Coq.ZArith.BinInt.Z.add_wd,Coq.ZArith.BinInt.Z.b2z_inj,Coq.ZArith.BinInt.Z.bit0_odd,Coq.ZArith.BinInt.Z.bits_0,Coq.ZArith.BinInt.Z.bits_above_log2,Coq.ZArith.BinInt.Z.bits_inj',Coq.ZArith.BinInt.Z.bits_inj_iff,Coq.ZArith.BinInt.Z.bits_inj_iff',Coq.ZArith.BinInt.Z.bits_m1,Coq.ZArith.BinInt.Z.bits_opp,Coq.ZArith.BinInt.Z.compare_antisym,Coq.ZArith.BinInt.Z.compare_spec,Coq.ZArith.BinInt.Z.compare_sub,Coq.ZArith.BinInt.Z.crossmul_le_addsquare,Coq.ZArith.BinInt.Z.div2_bits,Coq.ZArith.BinInt.Z.div_0_l,Coq.ZArith.BinInt.Z.div_1_r,Coq.ZArith.BinInt.Z.div_add,Coq.ZArith.BinInt.Z.div_div,Coq.ZArith.BinInt.Z.div_le_compat_l,Coq.ZArith.BinInt.Z.div_le_lower_bound,Coq.ZArith.BinInt.Z.div_le_mono,Coq.ZArith.BinInt.Z.div_le_upper_bound,Coq.ZArith.BinInt.Z.div_lt_upper_bound,Coq.ZArith.BinInt.Z.div_mod,Coq.ZArith.BinInt.Z.div_mod_unique,Coq.ZArith.BinInt.Z.div_mul,Coq.ZArith.BinInt.Z.div_mul_le,Coq.ZArith.BinInt.Z.div_opp_opp,Coq.ZArith.BinInt.Z.div_pos,Coq.ZArith.BinInt.Z.div_small,Coq.ZArith.BinInt.Z.div_unique,Coq.ZArith.BinInt.Z.div_unique_exact,Coq.ZArith.BinInt.Z.div_unique_neg,Coq.ZArith.BinInt.Z.div_unique_pos,Coq.ZArith.BinInt.Z.div_wd,Coq.ZArith.BinInt.Z.divide_1_l,Coq.ZArith.BinInt.Z.divide_1_r_nonneg,Coq.ZArith.BinInt.Z.divide_antisym_nonneg,Coq.ZArith.BinInt.Z.divide_gcd_iff,Coq.ZArith.BinInt.Z.divide_lcm_eq_r,Coq.ZArith.BinInt.Z.divide_lcm_iff,Coq.ZArith.BinInt.Z.divide_mul_l,Coq.ZArith.BinInt.Z.divide_pos_le,Coq.ZArith.BinInt.Z.divide_refl,Coq.ZArith.BinInt.Z.divide_wd,Coq.ZArith.BinInt.Z.eq_decidable,Coq.ZArith.BinInt.Z.eq_equiv,Coq.ZArith.BinInt.Z.eq_le_incl,Coq.ZArith.BinInt.Z.eq_mul_0,Coq.ZArith.BinInt.Z.eq_mul_0_l,Coq.ZArith.BinInt.Z.eq_mul_0_r,Coq.ZArith.BinInt.Z.eq_mul_1_nonneg,Coq.ZArith.BinInt.Z.eq_mul_1_nonneg',Coq.ZArith.BinInt.Z.eq_sym,Coq.ZArith.BinInt.Z.gcd_0_l_nonneg,Coq.ZArith.BinInt.Z.gcd_0_r_nonneg,Coq.ZArith.BinInt.Z.gcd_diag_nonneg,Coq.ZArith.BinInt.Z.gcd_divide_l,Coq.ZArith.BinInt.Z.gcd_divide_r,Coq.ZArith.BinInt.Z.gcd_mul_diag_l,Coq.ZArith.BinInt.Z.gcd_mul_mono_l_nonneg,Coq.ZArith.BinInt.Z.gcd_mul_mono_r_nonneg,Coq.ZArith.BinInt.Z.gcd_nonneg,Coq.ZArith.BinInt.Z.gcd_unique,Coq.ZArith.BinInt.Z.gcd_unique_alt,Coq.ZArith.BinInt.Z.gcd_wd,Coq.ZArith.BinInt.Z.ge_le,Coq.ZArith.BinInt.Z.ge_le_iff,Coq.ZArith.BinInt.Z.gt_lt_iff,Coq.ZArith.BinInt.Z.land_comm,Coq.ZArith.BinInt.Z.land_nonneg,Coq.ZArith.BinInt.Z.lbase,Coq.ZArith.BinInt.Z.lcm_1_l_nonneg,Coq.ZArith.BinInt.Z.lcm_1_r_nonneg,Coq.ZArith.BinInt.Z.lcm_diag_nonneg,Coq.ZArith.BinInt.Z.lcm_mul_mono_l_nonneg,Coq.ZArith.BinInt.Z.lcm_mul_mono_r_nonneg,Coq.ZArith.BinInt.Z.lcm_nonneg,Coq.ZArith.BinInt.Z.lcm_unique,Coq.ZArith.BinInt.Z.lcm_unique_alt,Coq.ZArith.BinInt.Z.ldiff_le,Coq.ZArith.BinInt.Z.ldiff_neg,Coq.ZArith.BinInt.Z.ldiff_spec,Coq.ZArith.BinInt.Z.ldiff_wd,Coq.ZArith.BinInt.Z.le_0_1,Coq.ZArith.BinInt.Z.le_0_mul,Coq.ZArith.BinInt.Z.le_0_sub,Coq.ZArith.BinInt.Z.le_add_le_sub_r,Coq.ZArith.BinInt.Z.le_antisymm,Coq.ZArith.BinInt.Z.le_decidable,Coq.ZArith.BinInt.Z.le_exists_sub,Coq.ZArith.BinInt.Z.le_ge,Coq.ZArith.BinInt.Z.le_ge_cases,Coq.ZArith.BinInt.Z.le_gt_cases,Coq.ZArith.BinInt.Z.le_ind,Coq.ZArith.BinInt.Z.le_le_add_le,Coq.ZArith.BinInt.Z.le_le_pred,Coq.ZArith.BinInt.Z.le_le_sub_lt,Coq.ZArith.BinInt.Z.le_le_succ_r,Coq.ZArith.BinInt.Z.le_lt_add_lt,Coq.ZArith.BinInt.Z.le_lt_trans,Coq.ZArith.BinInt.Z.le_lteq,Coq.ZArith.BinInt.Z.le_max_l,Coq.ZArith.BinInt.Z.le_mul_0,Coq.ZArith.BinInt.Z.le_mul_diag_l,Coq.ZArith.BinInt.Z.le_mul_diag_r,Coq.ZArith.BinInt.Z.le_ngt,Coq.ZArith.BinInt.Z.le_pred_l,Coq.ZArith.BinInt.Z.le_pred_lt,Coq.ZArith.BinInt.Z.le_preorder,Coq.ZArith.BinInt.Z.le_refl,Coq.ZArith.BinInt.Z.le_stepl,Coq.ZArith.BinInt.Z.le_stepr,Coq.ZArith.BinInt.Z.le_sub_0,Coq.ZArith.BinInt.Z.le_sub_le_add_r,Coq.ZArith.BinInt.Z.le_sub_nonneg,Coq.ZArith.BinInt.Z.le_succ_diag_r,Coq.ZArith.BinInt.Z.le_succ_l,Coq.ZArith.BinInt.Z.le_trans,Coq.ZArith.BinInt.Z.le_wd,Coq.ZArith.BinInt.Z.leb_le,Coq.ZArith.BinInt.Z.leb_spec,Coq.ZArith.BinInt.Z.lnot_shiftr,Coq.ZArith.BinInt.Z.lnot_spec,Coq.ZArith.BinInt.Z.log2_land,Coq.ZArith.BinInt.Z.log2_le_lin,Coq.ZArith.BinInt.Z.log2_le_mono,Coq.ZArith.BinInt.Z.log2_log2_up_spec,Coq.ZArith.BinInt.Z.log2_lor,Coq.ZArith.BinInt.Z.log2_lt_cancel,Coq.ZArith.BinInt.Z.log2_lt_lin,Coq.ZArith.BinInt.Z.log2_lt_pow2,Coq.ZArith.BinInt.Z.log2_lxor,Coq.ZArith.BinInt.Z.log2_mul_above,Coq.ZArith.BinInt.Z.log2_mul_pow2,Coq.ZArith.BinInt.Z.log2_nonneg,Coq.ZArith.BinInt.Z.log2_nonpos,Coq.ZArith.BinInt.Z.log2_pow2,Coq.ZArith.BinInt.Z.log2_spec,Coq.ZArith.BinInt.Z.log2_unique,Coq.ZArith.BinInt.Z.log2_up_1,Coq.ZArith.BinInt.Z.log2_up_eqn,Coq.ZArith.BinInt.Z.log2_up_eqn0,Coq.ZArith.BinInt.Z.log2_up_le_lin,Coq.ZArith.BinInt.Z.log2_up_le_mono,Coq.ZArith.BinInt.Z.log2_up_le_pow2,Coq.ZArith.BinInt.Z.log2_up_lt_lin,Coq.ZArith.BinInt.Z.log2_up_mul_above,Coq.ZArith.BinInt.Z.log2_up_mul_pow2,Coq.ZArith.BinInt.Z.log2_up_nonneg,Coq.ZArith.BinInt.Z.log2_up_nonpos,Coq.ZArith.BinInt.Z.log2_up_pos,Coq.ZArith.BinInt.Z.log2_up_pow2,Coq.ZArith.BinInt.Z.log2_up_spec,Coq.ZArith.BinInt.Z.log2_up_wd,Coq.ZArith.BinInt.Z.log2_wd,Coq.ZArith.BinInt.Z.lor_spec,Coq.ZArith.BinInt.Z.lt_0_1,Coq.ZArith.BinInt.Z.lt_0_mul,Coq.ZArith.BinInt.Z.lt_0_sub,Coq.ZArith.BinInt.Z.lt_1_2,Coq.ZArith.BinInt.Z.lt_1_mul_pos,Coq.ZArith.BinInt.Z.lt_decidable,Coq.ZArith.BinInt.Z.lt_eq_cases,Coq.ZArith.BinInt.Z.lt_exists_pred,Coq.ZArith.BinInt.Z.lt_exists_pred_strong,Coq.ZArith.BinInt.Z.lt_ge_cases,Coq.ZArith.BinInt.Z.lt_ind,Coq.ZArith.BinInt.Z.lt_irrefl,Coq.ZArith.BinInt.Z.lt_le_incl,Coq.ZArith.BinInt.Z.lt_le_pred,Coq.ZArith.BinInt.Z.lt_le_trans,Coq.ZArith.BinInt.Z.lt_lt_succ_r,Coq.ZArith.BinInt.Z.lt_mul_0,Coq.ZArith.BinInt.Z.lt_neq,Coq.ZArith.BinInt.Z.lt_nge,Coq.ZArith.BinInt.Z.lt_pred_l,Coq.ZArith.BinInt.Z.lt_sub_0,Coq.ZArith.BinInt.Z.lt_succ_diag_r,Coq.ZArith.BinInt.Z.lt_succ_pred,Coq.ZArith.BinInt.Z.lt_succ_r,Coq.ZArith.BinInt.Z.lt_trans,Coq.ZArith.BinInt.Z.lt_trichotomy,Coq.ZArith.BinInt.Z.lt_wd,Coq.ZArith.BinInt.Z.ltb_spec,Coq.ZArith.BinInt.Z.lxor_comm,Coq.ZArith.BinInt.Z.lxor_nonneg,Coq.ZArith.BinInt.Z.lxor_spec,Coq.ZArith.BinInt.Z.max_l,Coq.ZArith.BinInt.Z.max_le,Coq.ZArith.BinInt.Z.max_lub,Coq.ZArith.BinInt.Z.max_lub_l,Coq.ZArith.BinInt.Z.max_lub_r,Coq.ZArith.BinInt.Z.max_r,Coq.ZArith.BinInt.Z.max_spec,Coq.ZArith.BinInt.Z.min_glb,Coq.ZArith.BinInt.Z.min_glb_l,Coq.ZArith.BinInt.Z.min_glb_r,Coq.ZArith.BinInt.Z.min_l,Coq.ZArith.BinInt.Z.min_le,Coq.ZArith.BinInt.Z.min_r,Coq.ZArith.BinInt.Z.min_spec,Coq.ZArith.BinInt.Z.mod_bound_or,Coq.ZArith.BinInt.Z.mod_bound_pos,Coq.ZArith.BinInt.Z.mod_le,Coq.ZArith.BinInt.Z.mod_neg_bound,Coq.ZArith.BinInt.Z.mod_pos_bound,Coq.ZArith.BinInt.Z.mod_sign_mul,Coq.ZArith.BinInt.Z.mod_small,Coq.ZArith.BinInt.Z.mod_unique,Coq.ZArith.BinInt.Z.mod_unique_neg,Coq.ZArith.BinInt.Z.mod_unique_pos,Coq.ZArith.BinInt.Z.mul_0_l,Coq.ZArith.BinInt.Z.mul_0_r,Coq.ZArith.BinInt.Z.mul_1_l,Coq.ZArith.BinInt.Z.mul_1_r,Coq.ZArith.BinInt.Z.mul_add_distr_l,Coq.ZArith.BinInt.Z.mul_add_distr_r,Coq.ZArith.BinInt.Z.mul_assoc,Coq.ZArith.BinInt.Z.mul_cancel_l,Coq.ZArith.BinInt.Z.mul_comm,Coq.ZArith.BinInt.Z.mul_div_ge,Coq.ZArith.BinInt.Z.mul_div_le,Coq.ZArith.BinInt.Z.mul_eq_0_l,Coq.ZArith.BinInt.Z.mul_eq_0_r,Coq.ZArith.BinInt.Z.mul_id_l,Coq.ZArith.BinInt.Z.mul_le_mono_neg_l,Coq.ZArith.BinInt.Z.mul_le_mono_neg_r,Coq.ZArith.BinInt.Z.mul_le_mono_nonneg,Coq.ZArith.BinInt.Z.mul_le_mono_nonneg_l,Coq.ZArith.BinInt.Z.mul_le_mono_nonneg_r,Coq.ZArith.BinInt.Z.mul_le_mono_nonpos,Coq.ZArith.BinInt.Z.mul_le_mono_nonpos_l,Coq.ZArith.BinInt.Z.mul_le_mono_nonpos_r,Coq.ZArith.BinInt.Z.mul_le_mono_pos_l,Coq.ZArith.BinInt.Z.mul_le_mono_pos_r,Coq.ZArith.BinInt.Z.mul_lt_mono_neg_l,Coq.ZArith.BinInt.Z.mul_lt_mono_neg_r,Coq.ZArith.BinInt.Z.mul_lt_mono_nonneg,Coq.ZArith.BinInt.Z.mul_lt_mono_nonpos,Coq.ZArith.BinInt.Z.mul_lt_mono_pos_l,Coq.ZArith.BinInt.Z.mul_lt_mono_pos_r,Coq.ZArith.BinInt.Z.mul_max_distr_nonneg_l,Coq.ZArith.BinInt.Z.mul_max_distr_nonneg_r,Coq.ZArith.BinInt.Z.mul_max_distr_nonpos_l,Coq.ZArith.BinInt.Z.mul_max_distr_nonpos_r,Coq.ZArith.BinInt.Z.mul_min_distr_nonneg_l,Coq.ZArith.BinInt.Z.mul_min_distr_nonneg_r,Coq.ZArith.BinInt.Z.mul_min_distr_nonpos_l,Coq.ZArith.BinInt.Z.mul_min_distr_nonpos_r,Coq.ZArith.BinInt.Z.mul_neg_pos,Coq.ZArith.BinInt.Z.mul_nonneg_cancel_l,Coq.ZArith.BinInt.Z.mul_nonneg_cancel_r,Coq.ZArith.BinInt.Z.mul_nonneg_nonneg,Coq.ZArith.BinInt.Z.mul_nonneg_nonpos,Coq.ZArith.BinInt.Z.mul_nonpos_nonneg,Coq.ZArith.BinInt.Z.mul_nonpos_nonpos,Coq.ZArith.BinInt.Z.mul_opp_comm,Coq.ZArith.BinInt.Z.mul_opp_l,Coq.ZArith.BinInt.Z.mul_opp_opp,Coq.ZArith.BinInt.Z.mul_opp_r,Coq.ZArith.BinInt.Z.mul_pos_cancel_r,Coq.ZArith.BinInt.Z.mul_pos_neg,Coq.ZArith.BinInt.Z.mul_pos_pos,Coq.ZArith.BinInt.Z.mul_pow2_bits,Coq.ZArith.BinInt.Z.mul_pow2_bits_add,Coq.ZArith.BinInt.Z.mul_pred_quot_gt,Coq.ZArith.BinInt.Z.mul_pred_quot_lt,Coq.ZArith.BinInt.Z.mul_quot_ge,Coq.ZArith.BinInt.Z.mul_quot_le,Coq.ZArith.BinInt.Z.mul_reg_l,Coq.ZArith.BinInt.Z.mul_reg_r,Coq.ZArith.BinInt.Z.mul_shuffle0,Coq.ZArith.BinInt.Z.mul_shuffle1,Coq.ZArith.BinInt.Z.mul_shuffle3,Coq.ZArith.BinInt.Z.mul_sub_distr_l,Coq.ZArith.BinInt.Z.mul_sub_distr_r,Coq.ZArith.BinInt.Z.mul_succ_l,Coq.ZArith.BinInt.Z.mul_succ_quot_gt,Coq.ZArith.BinInt.Z.mul_succ_quot_lt,Coq.ZArith.BinInt.Z.mul_succ_r,Coq.ZArith.BinInt.Z.mul_wd,Coq.ZArith.BinInt.Z.neg_nonneg_cases,Coq.ZArith.BinInt.Z.neq_mul_0,Coq.ZArith.BinInt.Z.nle_gt,Coq.ZArith.BinInt.Z.nonpos_nonneg_cases,Coq.ZArith.BinInt.Z.nonpos_pos_cases,Coq.ZArith.BinInt.Z.one_succ,Coq.ZArith.BinInt.Z.ones_spec_high,Coq.ZArith.BinInt.Z.ones_spec_iff,Coq.ZArith.BinInt.Z.ones_spec_low,Coq.ZArith.BinInt.Z.opp_0,Coq.ZArith.BinInt.Z.opp_add_distr,Coq.ZArith.BinInt.Z.opp_inj,Coq.ZArith.BinInt.Z.opp_inj_wd,Coq.ZArith.BinInt.Z.opp_involutive,Coq.ZArith.BinInt.Z.opp_le_mono,Coq.ZArith.BinInt.Z.opp_lt_mono,Coq.ZArith.BinInt.Z.opp_neg_pos,Coq.ZArith.BinInt.Z.opp_nonneg_nonpos,Coq.ZArith.BinInt.Z.opp_nonpos_nonneg,Coq.ZArith.BinInt.Z.opp_pos_neg,Coq.ZArith.BinInt.Z.opp_wd,Coq.ZArith.BinInt.Z.order_induction_0,Coq.ZArith.BinInt.Z.pow_0_r,Coq.ZArith.BinInt.Z.pow_1_l,Coq.ZArith.BinInt.Z.pow_1_r,Coq.ZArith.BinInt.Z.pow_add_lower,Coq.ZArith.BinInt.Z.pow_add_r,Coq.ZArith.BinInt.Z.pow_add_upper,Coq.ZArith.BinInt.Z.pow_eq_0,Coq.ZArith.BinInt.Z.pow_gt_lin_r,Coq.ZArith.BinInt.Z.pow_inj_l,Coq.ZArith.BinInt.Z.pow_inj_r,Coq.ZArith.BinInt.Z.pow_le_mono,Coq.ZArith.BinInt.Z.pow_le_mono_l,Coq.ZArith.BinInt.Z.pow_le_mono_l_iff,Coq.ZArith.BinInt.Z.pow_le_mono_r,Coq.ZArith.BinInt.Z.pow_le_mono_r_iff,Coq.ZArith.BinInt.Z.pow_lt_mono_l,Coq.ZArith.BinInt.Z.pow_lt_mono_l_iff,Coq.ZArith.BinInt.Z.pow_lt_mono_r,Coq.ZArith.BinInt.Z.pow_lt_mono_r_iff,Coq.ZArith.BinInt.Z.pow_mul_l,Coq.ZArith.BinInt.Z.pow_mul_r,Coq.ZArith.BinInt.Z.pow_neg_r,Coq.ZArith.BinInt.Z.pow_nonneg,Coq.ZArith.BinInt.Z.pow_nonzero,Coq.ZArith.BinInt.Z.pow_odd_sgn,Coq.ZArith.BinInt.Z.pow_pos_nonneg,Coq.ZArith.BinInt.Z.pow_succ_r,Coq.ZArith.BinInt.Z.pow_wd,Coq.ZArith.BinInt.Z.pred_succ,Coq.ZArith.BinInt.Z.pred_wd,Coq.ZArith.BinInt.Z.quadmul_le_squareadd,Coq.ZArith.BinInt.Z.quot_add,Coq.ZArith.BinInt.Z.quot_add_l,Coq.ZArith.BinInt.Z.quot_div_nonneg,Coq.ZArith.BinInt.Z.quot_le_compat_l,Coq.ZArith.BinInt.Z.quot_le_lower_bound,Coq.ZArith.BinInt.Z.quot_le_mono,Coq.ZArith.BinInt.Z.quot_le_upper_bound,Coq.ZArith.BinInt.Z.quot_lt_upper_bound,Coq.ZArith.BinInt.Z.quot_mul,Coq.ZArith.BinInt.Z.quot_mul_le,Coq.ZArith.BinInt.Z.quot_opp_l,Coq.ZArith.BinInt.Z.quot_opp_opp,Coq.ZArith.BinInt.Z.quot_opp_r,Coq.ZArith.BinInt.Z.quot_pos,Coq.ZArith.BinInt.Z.quot_rem,Coq.ZArith.BinInt.Z.quot_rem_unique,Coq.ZArith.BinInt.Z.quot_small,Coq.ZArith.BinInt.Z.quot_unique,Coq.ZArith.BinInt.Z.quot_unique_exact,Coq.ZArith.BinInt.Z.quot_wd,Coq.ZArith.BinInt.Z.rbase,Coq.ZArith.BinInt.Z.rem_0_l,Coq.ZArith.BinInt.Z.rem_add,Coq.ZArith.BinInt.Z.rem_bound_pos,Coq.ZArith.BinInt.Z.rem_le,Coq.ZArith.BinInt.Z.rem_mod_nonneg,Coq.ZArith.BinInt.Z.rem_nonneg,Coq.ZArith.BinInt.Z.rem_nonpos,Coq.ZArith.BinInt.Z.rem_opp_l,Coq.ZArith.BinInt.Z.rem_opp_r,Coq.ZArith.BinInt.Z.rem_sign_mul,Coq.ZArith.BinInt.Z.rem_small,Coq.ZArith.BinInt.Z.rem_unique,Coq.ZArith.BinInt.Z.rem_wd,Coq.ZArith.BinInt.Z.setbit_eq,Coq.ZArith.BinInt.Z.setbit_neq,Coq.ZArith.BinInt.Z.sgn_0,Coq.ZArith.BinInt.Z.sgn_neg,Coq.ZArith.BinInt.Z.sgn_null,Coq.ZArith.BinInt.Z.sgn_null_iff,Coq.ZArith.BinInt.Z.sgn_pos,Coq.ZArith.BinInt.Z.sgn_spec,Coq.ZArith.BinInt.Z.shiftl_eq_0_iff,Coq.ZArith.BinInt.Z.shiftl_mul_pow2,Coq.ZArith.BinInt.Z.shiftl_shiftl,Coq.ZArith.BinInt.Z.shiftl_spec,Coq.ZArith.BinInt.Z.shiftl_spec_alt,Coq.ZArith.BinInt.Z.shiftl_spec_high,Coq.ZArith.BinInt.Z.shiftr_div_pow2,Coq.ZArith.BinInt.Z.shiftr_eq_0,Coq.ZArith.BinInt.Z.shiftr_mul_pow2,Coq.ZArith.BinInt.Z.shiftr_shiftl_r,Coq.ZArith.BinInt.Z.shiftr_shiftr,Coq.ZArith.BinInt.Z.shiftr_spec,Coq.ZArith.BinInt.Z.shiftr_spec_aux,Coq.ZArith.BinInt.Z.shiftr_wd,Coq.ZArith.BinInt.Z.sqrt_0,Coq.ZArith.BinInt.Z.sqrt_1,Coq.ZArith.BinInt.Z.sqrt_eq_succ_iff_square,Coq.ZArith.BinInt.Z.sqrt_le_lin,Coq.ZArith.BinInt.Z.sqrt_le_mono,Coq.ZArith.BinInt.Z.sqrt_le_square,Coq.ZArith.BinInt.Z.sqrt_lt_cancel,Coq.ZArith.BinInt.Z.sqrt_lt_square,Coq.ZArith.BinInt.Z.sqrt_mul_above,Coq.ZArith.BinInt.Z.sqrt_neg,Coq.ZArith.BinInt.Z.sqrt_nonneg,Coq.ZArith.BinInt.Z.sqrt_pred_square,Coq.ZArith.BinInt.Z.sqrt_spec,Coq.ZArith.BinInt.Z.sqrt_spec_alt,Coq.ZArith.BinInt.Z.sqrt_spec_nonneg,Coq.ZArith.BinInt.Z.sqrt_sqrt_up_exact,Coq.ZArith.BinInt.Z.sqrt_sqrt_up_spec,Coq.ZArith.BinInt.Z.sqrt_square,Coq.ZArith.BinInt.Z.sqrt_succ_le,Coq.ZArith.BinInt.Z.sqrt_succ_or,Coq.ZArith.BinInt.Z.sqrt_unique,Coq.ZArith.BinInt.Z.sqrt_unique',Coq.ZArith.BinInt.Z.sqrt_up_0,Coq.ZArith.BinInt.Z.sqrt_up_eq_succ_iff_square,Coq.ZArith.BinInt.Z.sqrt_up_eqn,Coq.ZArith.BinInt.Z.sqrt_up_eqn0,Coq.ZArith.BinInt.Z.sqrt_up_le_lin,Coq.ZArith.BinInt.Z.sqrt_up_le_mono,Coq.ZArith.BinInt.Z.sqrt_up_le_square,Coq.ZArith.BinInt.Z.sqrt_up_lt_cancel,Coq.ZArith.BinInt.Z.sqrt_up_lt_square,Coq.ZArith.BinInt.Z.sqrt_up_mul_above,Coq.ZArith.BinInt.Z.sqrt_up_nonneg,Coq.ZArith.BinInt.Z.sqrt_up_spec,Coq.ZArith.BinInt.Z.sqrt_up_square,Coq.ZArith.BinInt.Z.sqrt_up_succ_le,Coq.ZArith.BinInt.Z.sqrt_up_succ_or,Coq.ZArith.BinInt.Z.sqrt_up_succ_square,Coq.ZArith.BinInt.Z.sqrt_up_unique,Coq.ZArith.BinInt.Z.sqrt_up_wd,Coq.ZArith.BinInt.Z.sqrt_wd,Coq.ZArith.BinInt.Z.sqrtrem_spec,Coq.ZArith.BinInt.Z.square_add_le,Coq.ZArith.BinInt.Z.square_le_mono_nonneg,Coq.ZArith.BinInt.Z.square_le_mono_nonpos,Coq.ZArith.BinInt.Z.square_le_simpl_nonneg,Coq.ZArith.BinInt.Z.square_le_simpl_nonpos,Coq.ZArith.BinInt.Z.square_lt_mono_nonneg,Coq.ZArith.BinInt.Z.square_lt_mono_nonpos,Coq.ZArith.BinInt.Z.square_lt_simpl_nonneg,Coq.ZArith.BinInt.Z.square_lt_simpl_nonpos,Coq.ZArith.BinInt.Z.square_nonneg,Coq.ZArith.BinInt.Z.strong_right_induction,Coq.ZArith.BinInt.Z.sub_0_r,Coq.ZArith.BinInt.Z.sub_add,Coq.ZArith.BinInt.Z.sub_diag,Coq.ZArith.BinInt.Z.sub_le_mono_l,Coq.ZArith.BinInt.Z.sub_le_mono_r,Coq.ZArith.BinInt.Z.sub_nonneg_cases,Coq.ZArith.BinInt.Z.sub_nonpos_cases,Coq.ZArith.BinInt.Z.sub_opp_r,Coq.ZArith.BinInt.Z.sub_simpl_r,Coq.ZArith.BinInt.Z.succ_inj,Coq.ZArith.BinInt.Z.succ_le_mono,Coq.ZArith.BinInt.Z.succ_lt_mono,Coq.ZArith.BinInt.Z.succ_pred,Coq.ZArith.BinInt.Z.succ_wd,Coq.ZArith.BinInt.Z.testbit_even_succ,Coq.ZArith.BinInt.Z.testbit_neg_r,Coq.ZArith.BinInt.Z.testbit_odd_succ,Coq.ZArith.BinInt.Z.testbit_of_N',Coq.ZArith.BinInt.Z.testbit_ones_nonneg,Coq.ZArith.BinInt.Z.testbit_spec,Coq.ZArith.BinInt.Z.testbit_spec',Coq.ZArith.BinInt.Z.testbit_succ_r,Coq.ZArith.BinInt.Z.testbit_unique,Coq.ZArith.BinInt.Z.testbit_wd,Coq.ZArith.BinInt.Z.two_succ,Coq.ZArith.BinInt.Z2Pos.to_pos_nonpos,Coq.ZArith.BinInt.Zmult_integral,Coq.ZArith.BinInt.Zmult_integral_l,Coq.ZArith.Wf_Z.Z_lt_induction,Coq.ZArith.Wf_Z.Z_of_nat_complete,Coq.ZArith.Wf_Z.Z_of_nat_prop,Coq.ZArith.Wf_Z.Zlt_0_ind,Coq.ZArith.Wf_Z.Zlt_lower_bound_ind,Coq.ZArith.Wf_Z.natlike_ind,Coq.ZArith.Zabs.Zabs_nat_le,Coq.ZArith.Zabs.Zabs_nat_lt,Coq.ZArith.Zbool.Zle_bool_imp_le,Coq.ZArith.Zcomplements.sqr_pos,Coq.ZArith.Zdiv.Z_div_le,Coq.ZArith.Zdiv.Z_div_mod,Coq.ZArith.Zdiv.Z_div_mod_POS,Coq.ZArith.Zdiv.Z_div_mod_eq,Coq.ZArith.Zdiv.Z_div_pos,Coq.ZArith.Zdiv.Z_mod_lt,Coq.ZArith.Zdiv.Z_mult_div_ge,Coq.ZArith.Zdiv.Zdiv_0_r,Coq.ZArith.Zdiv.Zdiv_Zdiv,Coq.ZArith.Zdiv.Zdiv_le_compat_l,Coq.ZArith.Zdiv.Zdiv_le_lower_bound,Coq.ZArith.Zdiv.Zdiv_le_upper_bound,Coq.ZArith.Zdiv.Zdiv_lt_upper_bound,Coq.ZArith.Zdiv.Zdiv_mod_unique,Coq.ZArith.Zdiv.Zdiv_mult_le,Coq.ZArith.Zdiv.Zdiv_small,Coq.ZArith.Zdiv.Zdiv_unique,Coq.ZArith.Zdiv.Zdiv_unique_full,Coq.ZArith.Zdiv.Zmod_le,Coq.ZArith.Zdiv.Zmod_small,Coq.ZArith.Zdiv.Zmod_unique,Coq.ZArith.Zdiv.Zmod_unique_full,Coq.ZArith.Znat.Nat2Z.inj_succ,Coq.ZArith.Znat.Nat2Z.is_nonneg,Coq.ZArith.Znat.Z2N.id,Coq.ZArith.Znat.Z2N.inj,Coq.ZArith.Znat.Z2N.inj_add,Coq.ZArith.Znat.Z2N.inj_compare,Coq.ZArith.Znat.Z2N.inj_div,Coq.ZArith.Znat.Z2N.inj_iff,Coq.ZArith.Znat.Z2N.inj_le,Coq.ZArith.Znat.Z2N.inj_lt,Coq.ZArith.Znat.Z2N.inj_mul,Coq.ZArith.Znat.Z2N.inj_pow,Coq.ZArith.Znat.Z2N.inj_quot,Coq.ZArith.Znat.Z2N.inj_rem,Coq.ZArith.Znat.Z2N.inj_sub,Coq.ZArith.Znat.Z2N.inj_succ,Coq.ZArith.Znat.Z2Nat.id,Coq.ZArith.Znat.Z2Nat.inj,Coq.ZArith.Znat.Z2Nat.inj_add,Coq.ZArith.Znat.Z2Nat.inj_compare,Coq.ZArith.Znat.Z2Nat.inj_iff,Coq.ZArith.Znat.Z2Nat.inj_le,Coq.ZArith.Znat.Z2Nat.inj_lt,Coq.ZArith.Znat.Z2Nat.inj_mul,Coq.ZArith.Znat.Z2Nat.inj_sub,Coq.ZArith.Znat.Z2Nat.inj_succ,Coq.ZArith.Znat.Z_N_nat,Coq.ZArith.Znat.Zabs2N.abs_N_nonneg,Coq.ZArith.Znat.Zabs2N.inj_add,Coq.ZArith.Znat.Zabs2N.inj_compare,Coq.ZArith.Znat.Zabs2N.inj_le,Coq.ZArith.Znat.Zabs2N.inj_lt,Coq.ZArith.Znat.Zabs2N.inj_max,Coq.ZArith.Znat.Zabs2N.inj_min,Coq.ZArith.Znat.Zabs2N.inj_pow,Coq.ZArith.Znat.Zabs2N.inj_sub,Coq.ZArith.Znat.Zabs2N.inj_succ,Coq.ZArith.Znat.Zabs2Nat.abs_nat_nonneg,Coq.ZArith.Znat.Zabs2Nat.inj_add,Coq.ZArith.Znat.Zabs2Nat.inj_compare,Coq.ZArith.Znat.Zabs2Nat.inj_le,Coq.ZArith.Znat.Zabs2Nat.inj_lt,Coq.ZArith.Znat.Zabs2Nat.inj_sub,Coq.ZArith.Znat.Zabs2Nat.inj_succ,Coq.ZArith.Znumtheory.Bezout_intro,Coq.ZArith.Znumtheory.Z_0_1_more,Coq.ZArith.Znumtheory.Zdivide_le,Coq.ZArith.Znumtheory.Zdivide_mod,Coq.ZArith.Znumtheory.Zdivide_mod_minus,Coq.ZArith.Znumtheory.Zgcd_is_gcd,Coq.ZArith.Znumtheory.Zis_gcd_0,Coq.ZArith.Znumtheory.Zis_gcd_for_euclid,Coq.ZArith.Znumtheory.Zis_gcd_gcd,Coq.ZArith.Znumtheory.Zis_gcd_intro,Coq.ZArith.Znumtheory.prime_dec_aux_subproof,Coq.ZArith.Znumtheory.prime_dec_aux_subproof0,Coq.ZArith.Znumtheory.prime_dec_aux_subproof1,Coq.ZArith.Znumtheory.prime_ind,Coq.ZArith.Znumtheory.rel_prime_cross_prod,Coq.ZArith.Zorder.Zgt_square_simpl,Coq.ZArith.Zorder.Zle_0_minus_le,Coq.ZArith.Zorder.Zle_lt_or_eq,Coq.ZArith.Zorder.Zle_minus_le_0,Coq.ZArith.Zorder.Zle_succ_le,Coq.ZArith.Zorder.Zlt_square_simpl,Coq.ZArith.Zorder.Zmult_ge_reg_r,Coq.ZArith.Zorder.Zmult_gt_0_le_0_compat,Coq.ZArith.Zorder.Zmult_gt_0_le_compat_r,Coq.ZArith.Zorder.Zmult_gt_0_lt_0_reg_r,Coq.ZArith.Zorder.Zmult_gt_0_lt_reg_r,Coq.ZArith.Zorder.Zmult_gt_0_reg_l,Coq.ZArith.Zorder.Zmult_gt_reg_r,Coq.ZArith.Zorder.Zmult_le_0_reg_r,Coq.ZArith.Zorder.Zmult_le_compat,Coq.ZArith.Zorder.Zmult_le_compat_l,Coq.ZArith.Zorder.Zmult_le_compat_r,Coq.ZArith.Zorder.Zmult_le_reg_r,Coq.ZArith.Zorder.Zmult_lt_0_le_compat_r,Coq.ZArith.Zorder.Zmult_lt_0_le_reg_r,Coq.ZArith.Zorder.Zmult_lt_0_reg_r,Coq.ZArith.Zorder.Zmult_lt_compat,Coq.ZArith.Zorder.Zmult_lt_compat2,Coq.ZArith.Zorder.Zmult_lt_reg_r,Coq.ZArith.Zorder.Znot_gt_le,Coq.ZArith.Zorder.Znot_le_gt,Coq.ZArith.Zorder.Znot_lt_ge,Coq.ZArith.Zorder.Zplus_le_compat_l,Coq.ZArith.Zorder.Zplus_le_reg_l,Coq.ZArith.Zorder.Zplus_le_reg_r,Coq.ZArith.Zorder.dec_Zgt,Coq.ZArith.Zpower.Zdiv_rest_proofs_ind,Coq.ZArith.Zpower.Zdiv_rest_proofs_sind,Coq.ZArith.Zpower.Zpower_nat_Zpower,Coq.ZArith.Zpower.two_p_S,Coq.ZArith.Zpower.two_p_gt_ZERO,Coq.ZArith.Zpower.two_p_is_exp,Coq.ZArith.Zpower.two_p_pred,Coq.ZArith.auxiliary.Zegal_left,Coq.ZArith.auxiliary.Zge_left,Coq.ZArith.auxiliary.Zgt_left,Coq.ZArith.auxiliary.Zle_left,Coq.ZArith.auxiliary.Zle_left_rev,Coq.ZArith.auxiliary.Zle_mult_approx,Coq.ZArith.auxiliary.Zlt_left,Coq.ZArith.auxiliary.Zmult_le_approx,Coq.ZArith.auxiliary.Zne_left,Coq.omega.OmegaLemmas.OMEGA1,Coq.omega.OmegaLemmas.OMEGA17,Coq.omega.OmegaLemmas.OMEGA2,Coq.omega.OmegaLemmas.OMEGA3,Coq.omega.OmegaLemmas.OMEGA6,Coq.omega.OmegaLemmas.OMEGA7,Coq.omega.OmegaLemmas.OMEGA8,Coq.omega.OmegaLemmas.fast_OMEGA10,Coq.omega.OmegaLemmas.fast_OMEGA11,Coq.omega.OmegaLemmas.fast_OMEGA12,Coq.omega.OmegaLemmas.fast_OMEGA13,Coq.omega.OmegaLemmas.fast_OMEGA14,Coq.omega.OmegaLemmas.fast_OMEGA15,Coq.omega.OmegaLemmas.fast_OMEGA16,Coq.omega.OmegaLemmas.fast_Zmult_assoc_reverse,Coq.omega.OmegaLemmas.fast_Zmult_comm,Coq.omega.OmegaLemmas.fast_Zopp_eq_mult_neg_1,Coq.omega.OmegaLemmas.fast_Zopp_mult_distr_r,Coq.omega.OmegaLemmas.fast_Zopp_plus_distr,Coq.omega.OmegaLemmas.fast_Zplus_assoc,Coq.omega.OmegaLemmas.fast_Zplus_assoc_reverse,Coq.omega.OmegaLemmas.fast_Zplus_comm,Coq.omega.OmegaLemmas.fast_Zplus_permute,Coq.omega.OmegaLemmas.fast_Zred_factor0,Coq.omega.OmegaLemmas.fast_Zred_factor2,Coq.omega.OmegaLemmas.fast_Zred_factor3,Coq.omega.OmegaLemmas.fast_Zred_factor4,Coq.omega.OmegaLemmas.fast_Zred_factor5,Coq.omega.OmegaLemmas.fast_Zred_factor6,Coq.omega.OmegaLemmas.intro_Z,Coq.omega.OmegaLemmas.new_var,Coq.omega.PreOmega.Z.rem_bound_neg_neg,Coq.omega.PreOmega.Z.rem_bound_neg_pos,Coq.omega.PreOmega.Z.rem_bound_pos_neg,Coq.omega.PreOmega.Z.rem_bound_pos_pos,$adef_Coq.PArith.BinPos.Pos.SqrtSpec_$a2,$adef_Coq.Reals.Rdefinitions.IZR_$a1,$adef_Coq.Init.Datatypes.None_$a1,$adef_Coq.ZArith.BinIntDef.Z.to_nat_$a1,$adef_Coq.NArith.BinNat.N.lt_$a2,$adef_Coq.ZArith.BinIntDef.Z.of_N_$a1,$adef_Coq.ZArith.BinIntDef.Z.modulo_$a2,$adef_Coq.Init.Datatypes.BoolSpec_$a3,$adef_Coq.setoid_ring.Ring_polynom.mk_monpol_list_$a10,$adef_Coq.ZArith.BinIntDef.Z.lxor_$a2,$adef_Coq.Reals.Rfunctions.ZintPos_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEc_$a2,$adef_Coq.ZArith.BinIntDef.Z.log2_$a1,$adef_Coq.ZArith.BinIntDef.Z.sgn_$a1,$adef_Coq.setoid_ring.Ring_polynom.PEmul_$a3,$adef_Coq.setoid_ring.Ring_polynom.Pc_$a2,$adef_Coq.NArith.BinNatDef.N.div_$a2,$adef_Coq.setoid_ring.Ring_polynom.vmon_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pol_$a1,$adef_Coq.Reals.Rdefinitions.IPR_$a1,$adef_Coq.ZArith.BinIntDef.Z.pred_$a1,$adef_Coq.Init.Nat.compare_$a2,$adef_$_prop_34425_$a1,$adef_Coq.Init.Specif.sig_$a2,$adef_Coq.ZArith.BinIntDef.Z.leb_$a2,$adef_Coq.ZArith.BinIntDef.Z.testbit_$a1,$adef_Coq.PArith.BinPosDef.Pos.pred_double_$a1,$adef_Coq.ZArith.BinIntDef.Z.mul_$a2,$adef_Coq.PArith.BinPosDef.Pos.iter_$a4,$adef_Coq.ZArith.BinIntDef.Z.sqrt_$a1,$adef_$_lam_68508_$a1,$adef_$_lam_14596_$a12,$adef_Coq.Init.Specif.sumbool_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEsub_$a3,$adef_$_lam_18639_$a1,$adef_Coq.Init.Nat.max_$a2,$adef_Coq.PArith.BinPosDef.Pos.pred_N_$a1,$adef_Coq.ZArith.Zpower.Zpower_nat_$a1,$adef_$_lam_300_$a3,$adef_Coq.Relations.Relation_Definitions.relation_$a1,$adef_Coq.ZArith.BinIntDef.Z.eqb_$a2,$adef_Coq.NArith.BinNatDef.N.sub_$a2,$adef_$_lam_59478_$a4,$adef_Coq.setoid_ring.Ring_polynom.Peq_$a4,$adef_Coq.setoid_ring.Ring_polynom.PExpr_$a1,$adef_Coq.Init.Datatypes.orb_$a2,$adef_Coq.Init.Datatypes.CompOpp_$a1,$adef_Coq.ZArith.Zpower.two_power_pos_$a1,$adef_Coq.ZArith.BinIntDef.Z.pos_div_eucl_$a2,$adef_$_lam_259_$a2,$adef_Coq.PArith.BinPosDef.Pos.iter_$a3,$adef_Coq.ZArith.BinInt.Z.log2_up_$a1,$adef_Coq.Reals.Rdefinitions.Rle_$a2,$adef_$_let_1_s_19231_$a1,$adef_Coq.ZArith.Zpower.Zdiv_rest_proofs_rect_$a5,$adef_Coq.QArith.QArith_base.Qle_$a2,$adef_Coq.Reals.Rfunctions.Z_spec_$a2,$adef_Coq.ZArith.BinIntDef.Z.to_N_$a1,$adef_Coq.ZArith.BinInt.Z.b2z_$a1,$adef_Coq.Init.Datatypes.nil_$a1,$adef_Coq.ZArith.Zpower.shift_pos_$a2,$adef_Coq.NArith.BinNatDef.N.max_$a2,$adef_Coq.Reals.Rdefinitions.Rmult_$a2,$adef_Coq.Reals.Rfunctions.ZintNeg_$a2,$adef_Coq.ZArith.Znumtheory.Bezout_$a3,$adef_Coq.Numbers.BinNums.Npos_$a1,$adef_Coq.Numbers.BinNums.xI_$a1,$adef_$_lam_14596_$a11,$adef_Coq.ZArith.BinIntDef.Z.sqrtrem_$a1,$adef_Coq.ZArith.Zeven.Zodd_$a1,$adef_Coq.ZArith.BinIntDef.Z.ltb_$a2,$adef_Coq.ZArith.BinIntDef.Z.abs_nat_$a1,$adef_Coq.ZArith.BinIntDef.Z.to_pos_$a1,$adef_Coq.Init.Datatypes.negb_$a1,$adef_Coq.PArith.BinPosDef.Pos.div2_$a1,$adef_Coq.Reals.Rdefinitions.Ropp_$a1,$adef_Coq.Init.Datatypes.nat_rect_$a3,$adef_Coq.ZArith.BinIntDef.Z.mul_$a1,$adef_Coq.ZArith.BinIntDef.Z.succ_$a1,$adef_Coq.Init.Nat.add_$a2,$adef_Coq.Classes.Morphisms.Proper_$a3,$adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2,$adef_Coq.Init.Specif.right_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3,$adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2,$adef_Coq.PArith.BinPosDef.Pos.div2_up_$a1,$adef_Coq.PArith.BinPosDef.Pos.sqrt_$a1,$adef_Coq.ZArith.BinIntDef.Z.odd_$a1,$adef_Coq.Init.Datatypes.S_$a1,$adef_Coq.setoid_ring.Ring_polynom.zmon_$a2,$adef_$_case_Coq.Init.Datatypes.nat$32090_$a1,$adef_Coq.ZArith.BinIntDef.Z.add_$a2,$adef_$_case_Coq.Init.Datatypes.prod$16639_$a2,$adef_Coq.PArith.BinPosDef.Pos.sqrtrem_$a1,$adef_$_fix_413_1_add_carry_$a2,$adef_Coq.Reals.Rdefinitions.Rlt_$a2,$adef_Coq.ZArith.BinIntDef.Z.sub_$a2,$adef_Coq.ZArith.Zpower.Zpower_nat_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEopp_$a2,$adef_Coq.ZArith.ZArith_dec.Z_zerop_$a1,$adef_$_prop_35229_$a2,$adef_Coq.ZArith.BinInt.Z.gt_$a2,$adef_Coq.Classes.RelationClasses.Symmetric_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEO_$a1,$adef_Coq.Numbers.BinNums.xO_$a1,$adef_$_lam_68508_$a2,$adef_Coq.ZArith.Zdiv.Remainder_$a2,$adef_Coq.Init.Wf.Acc_rect_$a5,$adef_Coq.ZArith.Zpower.Zdiv_rest_proof_$a4,$adef_Coq.Init.Wf.Acc_$a3,$adef_Coq.NArith.BinNatDef.N.of_nat_$a1,$adef_$_lam_300_$a2,$adef_Coq.ZArith.BinInt.Z.ge_$a2,$adef_Coq.ZArith.Zbool.Zeq_bool_$a2,$adef_Coq.QArith.QArith_base.Qmake_$a2,$adef_$_lam_259_$a3,$adef_Coq.setoid_ring.Ring_polynom.PEX_$a2,$adef_Coq.NArith.BinNatDef.N.min_$a2,$adef_Coq.ZArith.Znumtheory.Zis_gcd_$a3,$adef_Coq.PArith.BinPosDef.Pos.size_$a1,$adef_Coq.PArith.BinPosDef.Pos.iter_op_$a4,$adef_Coq.setoid_ring.Ring_polynom.norm_aux_$a9,$adef_Coq.Init.Datatypes.andb_$a2,$adef_Coq.Init.Peano.lt_$a2,$adef_Coq.ZArith.BinIntDef.Z.max_$a2,$adef_Coq.PArith.BinPos.Pos.le_$a2,$adef_Coq.Init.Nat.mul_$a2,$adef_Coq.Init.Peano.le_$a2,$adef_Coq.Classes.RelationClasses.Equivalence_$a2,$adef_Coq.Logic.Decidable.decidable_$a1,$adef_Coq.Init.Datatypes.snd_$a3,$adef_Coq.ZArith.BinInt.Z.eqf_$a2,$adef_Coq.PArith.BinPos.Pos.lt_$a2,$adef_Coq.ZArith.BinIntDef.Z.gcd_$a2,$adef_Coq.NArith.BinNatDef.N.testbit_$a2,$adef_Coq.PArith.BinPosDef.Pos.to_nat_$a1,$adef_Coq.ZArith.Zpower.two_p_$a1,$adef_Coq.ZArith.BinIntDef.Z.abs_N_$a1,$adef_Coq.Init.Datatypes.nat_rect_$a1,$adef_Coq.ZArith.Znumtheory.prime_$a1,$adef_$_lam_18639_$a2,$adef_$_prop_19713_$a2,$adef_Coq.QArith.QArith_base.Qnum_$a1,$adef_Coq.setoid_ring.Ring_polynom.PNSubstL_$a11,$adef_Coq.ZArith.BinIntDef.Z.land_$a2,$adef_Coq.PArith.BinPosDef.Pos.succ_$a1,$adef_Coq.ZArith.BinIntDef.Z.shiftr_$a2,$adef_Coq.Init.Wf.well_founded_induction_type_$a5,$adef_Coq.Init.Datatypes.prod_$a2,$adef_Coq.ZArith.BinInt.Z.eq_dec_$a2,$adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a12,$adef_Coq.ZArith.BinIntDef.Z.compare_$a2,$adef_$_let_11_subst_l_14524_$a10,$adef_Coq.QArith.QArith_base.Qden_$a1,$adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a1,$adef_Coq.ZArith.BinIntDef.Z.testbit_$a2,$adef_$_lam_59478_$a6,$adef_Coq.ZArith.BinInt.Z.lt_$a2,$adef_Coq.PArith.BinPosDef.Pos.eqb_$a2,$adef_Coq.ZArith.BinIntDef.Z.opp_$a1,$adef_Coq.Numbers.BinNums.Zneg_$a1,$adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3,$adef_Coq.NArith.BinNatDef.N.to_nat_$a1,$adef_Coq.ZArith.BinIntDef.Z.double_$a1,$adef_Coq.NArith.BinNatDef.N.pow_$a2,$adef_Coq.setoid_ring.Ring_polynom.PX_$a4,$adef_Coq.Init.Datatypes.nat_rec_$a1,$adef_Coq.PArith.BinPosDef.Pos.sub_mask_$a2,$adef_Coq.ZArith.BinInt.Z.ones_$a1,$adef_$_prop_13363_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEI_$a1,$adef_Coq.NArith.BinNatDef.N.pos_div_eucl_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3,$adef_Coq.Init.Datatypes.CompareSpec_$a4,$adef_Coq.Init.Datatypes.xorb_$a2,$adef_Coq.NArith.BinNatDef.N.modulo_$a2,$adef_Coq.ZArith.Znumtheory.Euclid_intro_$a5,$adef_$_case_Coq.Init.Datatypes.prod$16654_$a2,$adef_Coq.Classes.Morphisms.respectful_$a4,$adef_Coq.ZArith.BinIntDef.Z.abs_$a1,$adef_Coq.ZArith.BinInt.Z.setbit_$a2,$adef_Coq.NArith.BinNatDef.N.succ_$a1,$adef_Coq.ZArith.BinIntDef.Z.succ_double_$a1,$adef_$_let_2_s_19729_$a1,$adef_Coq.Init.Datatypes.nat_rect_$a4,$adef_Coq.ZArith.BinIntDef.Z.rem_$a2,$adef_Coq.PArith.BinPosDef.Pos.mul_$a2,$adef_Coq.PArith.BinPosDef.Pos.testbit_$a2,$adef_Coq.ZArith.Znumtheory.rel_prime_$a2,$adef_Coq.NArith.BinNatDef.N.mul_$a2,$adef_Coq.Init.Specif.exist_$a3,$adef_Coq.ZArith.BinIntDef.Z.ldiff_$a2,$adef_Coq.ZArith.BinInt.Z.le_$a2,$adef_Coq.Reals.Rpow_def.pow_$a2,$adef_$_case_Coq.Numbers.BinNums.Z$32085_$a3,$adef_Coq.PArith.BinPosDef.Pos.compare_cont_$a1,$adef_Coq.ZArith.BinIntDef.Z.quot_$a2,$adef_Coq.Init.Wf.well_founded_$a2,$adef_Coq.Init.Datatypes.cons_$a3,$adef_Coq.ZArith.BinIntDef.Z.div2_$a1,$adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1,$adef_Coq.Init.Datatypes.pair_$a4,$adef_Coq.ZArith.BinIntDef.Z.pred_double_$a1,$adef_Coq.ZArith.BinIntDef.Z.shiftl_$a2,$adef_Coq.PArith.BinPosDef.Pos.IsPos_$a1,$adef_$_prop_34426_$a1,$adef_Coq.ZArith.BinInt.Z.sqrt_up_$a1,$adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a2,$adef_Coq.Init.Datatypes.Some_$a2,$adef_$_lam_18637_$a1,$adef_Coq.Numbers.BinNums.Zpos_$a1,$adef_Coq.Init.Datatypes.list_$a1,$adef_Coq.ZArith.BinInt.Z.lnot_$a1,$adef_Coq.Init.Nat.sub_$a2,$adef_Coq.NArith.BinNatDef.N.add_$a2,$adef_Coq.ZArith.BinInt.Z.divide_$a2,$adef_Coq.PArith.BinPosDef.Pos.gcd_$a2,$adef_Coq.Reals.Rfunctions.ZintNull_$a1,$adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a11,$adef_Coq.ZArith.Znumtheory.Euclid_$a2,$adef_Coq.PArith.BinPosDef.Pos.sub_$a2,$adef_Coq.NArith.BinNatDef.N.compare_$a2,$adef_Coq.Init.Datatypes.fst_$a3,$adef_$_case_Coq.Init.Datatypes.prod$964_$a1,$adef_Coq.setoid_ring.Ring_polynom.mon_of_pol_$a4,$adef_Coq.ZArith.BinIntDef.Z.quotrem_$a2,$adef_Coq.ZArith.BinIntDef.Z.min_$a2,$adef_Coq.ZArith.BinInt.Zne_$a2,$adef_Coq.PArith.BinPosDef.Pos.compare_$a2,$adef_Coq.ZArith.BinIntDef.Z.div_$a2,$adef_$_case_Coq.Init.Datatypes.nat$32068_$a3,$adef_Coq.Init.Specif.left_$a2,$adef_Coq.ZArith.BinIntDef.Z.pow_$a2,$adef_Coq.ZArith.BinInt.Z.Odd_$a1,$adef_Coq.NArith.BinNat.N.le_$a2,$adef_Coq.Classes.RelationClasses.PreOrder_$a2,$adef_Coq.ZArith.BinInt.Z.lcm_$a2,$adef_Coq.ZArith.BinIntDef.Z.lor_$a2,$adef_Coq.ZArith.Zpower.Zdiv_rest_proofs_$a2,$adef_Coq.PArith.BinPosDef.Pos.of_succ_nat_$a1,$adef_Coq.PArith.BinPosDef.Pos.add_$a2,$tdef_$_type_19197,$tdef_$_type_65103,$tdef_$_type_19160,$tdef_$_type_13192,$tdef_Coq.ZArith.Znumtheory.Euclid,$tdef_$_type_13361,$tdef_$_type_19325,$tdef_$_type_31442,$tdef_$_type_410,$tdef_$_type_12,$tdef_$_type_59418,$tdef_$_type_19295,$tdef_Coq.Init.Datatypes.bool,$tdef_$_type_18949,$tdef_Coq.Init.Datatypes.list,$tdef_$_type_16391,$tdef_$_type_16412,$tdef_$_type_956,$tdef_$_type_19822,$tdef_Coq.Structures.OrdersTac.ord,$tdef_$_type_14746,$tdef_$_type_13871,$tdef_$_type_60503,$tdef_$_type_19321,$tdef_$_type_60221,$tdef_$_type_13849,$tdef_Coq.setoid_ring.Ring_polynom.Mon,$tdef_Coq.Init.Datatypes.comparison,$tdef_$_type_59295,$tdef_$_type_19459,$tdef_$_type_13189,$tdef_Coq.Numbers.BinNums.N,$tdef_$_type_31256,$tdef_Coq.Init.Specif.sumbool,$tdef_$_type_13657,$tdef_Coq.Reals.Rdefinitions.R,$tdef_$_type_399,$tdef_$_type_117,$tdef_$_type_68505,$tdef_$_type_13229,$tdef_$_type_68565,$tdef_$_type_57851,$tdef_$_type_19311,$tdef_$_type_45,$tdef_$_type_68539,$tdef_$_type_471,$tdef_$_type_323,$tdef_$_type_14906,$tdef_$_type_61,$tdef_$_type_59662,$tdef_Coq.Init.Datatypes.unit,$tdef_$_type_13227,$tdef_$_type_13209,$tdef_Coq.Init.Specif.sig,$tdef_$_type_16422,$tdef_$_type_19318,$tdef_$_type_16816,$tdef_$_type_19818,$tdef_$_type_30,$tdef_$_type_401,$tdef_$_type_18953,$tdef_$_type_74,$tdef_$_type_90,$tdef_Prop,$tdef_$_type_22011,$tdef_$_type_21994,$tdef_$_type_286,$tdef_$_type_443,$tdef_$_type_13186,$tdef_$_type_13214,$tdef_$_type_22008,$tdef_$_type_14048,$tdef_Coq.Reals.Rfunctions.Z_spec,$tdef_$_type_392,$tdef_$_type_59635,$tdef_Coq.ZArith.Zpower.Zdiv_rest_proofs,$tdef_$_type_59653,$tdef_$_type_35232,$tdef_$_type_18888,$tdef_$_type_18982,$tdef_$_type_34421,$tdef_$_type_22003,$tdef_$_type_18641,$tdef_$_type_59565,$tdef_$_type_19222,$tdef_$_type_13869,$tdef_$_type_13340,$tdef_$_type_16414,$tdef_$_type_14506,$tdef_$_type_13636,$tdef_$_type_59522,$tdef_$_type_515,$tdef_$_type_60511,$tdef_$_type_19307,$tdef_$_type_19298,$tdef_$_type_31347,$tdef_$_type_16853,$tdef_$_type_59578,$tdef_$_type_13342,$tdef_$_type_94,$tdef_$_type_376,$tdef_$_type_14728,$tdef_Coq.setoid_ring.Ring_polynom.Pol,$tdef_$_type_19220,$tdef_$_type_13885,$tdef_Coq.Numbers.BinNums.Z,$tdef_$_type_13874,$tdef_$_type_18872,$tdef_Coq.QArith.QArith_base.Q,$tdef_Coq.Numbers.BinNums.positive,$tdef_$_type_19204,$tdef_Coq.Init.Datatypes.nat,$tdef_$_type_59575,$tdef_$_type_14511,$tdef_$_type_13234,$tdef_$_type_68531,$tdef_$_type_19090,$tdef_$_type_59550,$tdef_Coq.Init.Datatypes.prod,$tdef_Coq.setoid_ring.Ring_polynom.PExpr,$tdef_$_type_59528,$tdef_$_type_18835,$tdef_$_type_68555,$tdef_$_type_19157,$tdef_$_type_97,$tdef_$_type_13315,$tdef_$_type_14243,$tdef_Type,$tdef_Coq.PArith.BinPosDef.Pos.mask,$tdef_$_type_14503,$tdef_$_type_60515,$tdef_$_type_60500,$tdef_$_type_16386,$tdef_$_type_13335,$tdef_$_type_525,$tdef_$_type_25,$tdef_$_type_14254,$tdef_$_type_34423,$tdef_$_type_245,$tdef_$_type_18997] % 6.23/6.56 =============================================================== % 6.23/6.56 % 6.23/6.56 Combined formula: 1727 axiom(s) => conjecture % 6.23/6.56 % 6.23/6.56 % Equality/functions detected -> nanoCoP oracle mode % 6.23/6.56 nanoCoP : % 6.23/6.56 % 4,360,862 inferences, 4.244 CPU in 4.244 seconds (100% CPU, 1027590 Lips) % 6.23/6.56 % 6.23/6.56 % nanoCoP proof (equality/functions) % 6.23/6.56 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 6.23/6.56 % 6.23/6.56 % SZS output end Proof %------------------------------------------------------------------------------