%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SEV644+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 : n023.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:50 PM UTC 2026 % Result : Theorem 15.66s 15.87s % Output : Proof 15.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SEV644+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.15/0.33 % Computer : n023.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 11 14:05:55 EDT 2026 % 0.15/0.33 % CPUTime : % 15.66/15.87 % SZS status Theorem % 15.66/15.87 % SZS output start Proof % 15.66/15.88 % 15.66/15.88 =============================================================== % 15.66/15.88 TPTP Problem: _HAMMER_GOAL (conjecture with 2363 axiom(s)) % 15.66/15.88 Axioms: [_HAMMER_COQ_TRUE,_HAMMER_COQ_FALSE,_HAMMER_COQ_TYPE_TYPE,$_case_Coq.Init.Datatypes.bool$164137,$_case_Coq.Init.Datatypes.bool$164198,$_case_Coq.Init.Datatypes.bool$164239,$_case_Coq.Init.Datatypes.bool$164264,$_case_Coq.Init.Datatypes.bool$164277,$_case_Coq.Init.Datatypes.bool$164282,$_case_Coq.Init.Datatypes.bool$166575,$_case_Coq.Init.Datatypes.bool$168311,$_case_Coq.Init.Datatypes.bool$78562,$_def_$_let_11_subst_l_1291,$_def_Coq.Arith.EqNat.eq_nat,$_def_Coq.Arith.PeanoNat.Nat.Even,$_def_Coq.Arith.PeanoNat.Nat.Odd,$_def_Coq.Arith.PeanoNat.Nat.b2n,$_def_Coq.Arith.PeanoNat.Nat.divide,$_def_Coq.Arith.PeanoNat.Nat.eqf,$_def_Coq.Arith.PeanoNat.Nat.le_alt,$_def_Coq.Bool.Bool.Is_true,$_def_Coq.Bool.Bool.eqb,$_def_Coq.Bool.Bool.leb,$_def_Coq.Bool.Bvector.Bvector,$_def_Coq.FSets.FSetPositive.PositiveSet.Empty,$_def_Coq.FSets.FSetPositive.PositiveSet.Equal,$_def_Coq.FSets.FSetPositive.PositiveSet.Exists,$_def_Coq.FSets.FSetPositive.PositiveSet.For_all,$_def_Coq.FSets.FSetPositive.PositiveSet.In,$_def_Coq.FSets.FSetPositive.PositiveSet.Subset,$_def_Coq.FSets.FSetPositive.PositiveSet.cardinal,$_def_Coq.FSets.FSetPositive.PositiveSet.compare_bool,$_def_Coq.FSets.FSetPositive.PositiveSet.elt,$_def_Coq.FSets.FSetPositive.PositiveSet.empty,$_def_Coq.FSets.FSetPositive.PositiveSet.equal,$_def_Coq.FSets.FSetPositive.PositiveSet.fold,$_def_Coq.FSets.FSetPositive.PositiveSet.is_empty,$_def_Coq.FSets.FSetPositive.PositiveSet.mem,$_def_Coq.FSets.FSetPositive.PositiveSet.rev,$_def_Coq.FSets.FSetPositive.PositiveSet.rev_append,$_def_Coq.FSets.FSetPositive.PositiveSet.singleton,$_def_Coq.FSets.FSetPositive.PositiveSet.t,$_def_Coq.FSets.FSetPositive.PositiveSet.union,$_def_Coq.Init.Datatypes.CompOpp,$_def_Coq.Init.Datatypes.CompSpecT,$_def_Coq.Init.Datatypes.andb,$_def_Coq.Init.Datatypes.app,$_def_Coq.Init.Datatypes.fst,$_def_Coq.Init.Datatypes.implb,$_def_Coq.Init.Datatypes.length,$_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.div,$_def_Coq.Init.Nat.div2,$_def_Coq.Init.Nat.double,$_def_Coq.Init.Nat.eqb,$_def_Coq.Init.Nat.even,$_def_Coq.Init.Nat.gcd,$_def_Coq.Init.Nat.land,$_def_Coq.Init.Nat.leb,$_def_Coq.Init.Nat.log2,$_def_Coq.Init.Nat.ltb,$_def_Coq.Init.Nat.max,$_def_Coq.Init.Nat.min,$_def_Coq.Init.Nat.mul,$_def_Coq.Init.Nat.odd,$_def_Coq.Init.Nat.pow,$_def_Coq.Init.Nat.pred,$_def_Coq.Init.Nat.shiftl,$_def_Coq.Init.Nat.shiftr,$_def_Coq.Init.Nat.sqrt,$_def_Coq.Init.Nat.sub,$_def_Coq.Init.Nat.testbit,$_def_Coq.Init.Peano.ge,$_def_Coq.Init.Peano.gt,$_def_Coq.Init.Peano.lt,$_def_Coq.Init.Specif.proj1_sig,$_def_Coq.Init.Specif.projT1,$_def_Coq.Init.Specif.projT2,$_def_Coq.Lists.List.In,$_def_Coq.Lists.List.existsb,$_def_Coq.Lists.List.fold_right,$_def_Coq.Lists.List.forallb,$_def_Coq.Lists.List.map,$_def_Coq.Lists.List.nth,$_def_Coq.Lists.List.tl,$_def_Coq.Lists.SetoidList.compat_bool,$_def_Coq.Lists.SetoidList.equivlistA,$_def_Coq.Logic.Decidable.decidable,$_def_Coq.NArith.BinNat.N.b2n,$_def_Coq.NArith.BinNat.N.divide,$_def_Coq.NArith.BinNat.N.eqf,$_def_Coq.NArith.BinNat.N.le,$_def_Coq.NArith.BinNat.N.le_alt,$_def_Coq.NArith.BinNat.N.lt,$_def_Coq.NArith.BinNatDef.N.add,$_def_Coq.NArith.BinNatDef.N.compare,$_def_Coq.NArith.BinNatDef.N.div,$_def_Coq.NArith.BinNatDef.N.double,$_def_Coq.NArith.BinNatDef.N.eqb,$_def_Coq.NArith.BinNatDef.N.even,$_def_Coq.NArith.BinNatDef.N.gcd,$_def_Coq.NArith.BinNatDef.N.land,$_def_Coq.NArith.BinNatDef.N.leb,$_def_Coq.NArith.BinNatDef.N.log2,$_def_Coq.NArith.BinNatDef.N.lor,$_def_Coq.NArith.BinNatDef.N.ltb,$_def_Coq.NArith.BinNatDef.N.lxor,$_def_Coq.NArith.BinNatDef.N.max,$_def_Coq.NArith.BinNatDef.N.min,$_def_Coq.NArith.BinNatDef.N.modulo,$_def_Coq.NArith.BinNatDef.N.mul,$_def_Coq.NArith.BinNatDef.N.odd,$_def_Coq.NArith.BinNatDef.N.of_nat,$_def_Coq.NArith.BinNatDef.N.pow,$_def_Coq.NArith.BinNatDef.N.pred,$_def_Coq.NArith.BinNatDef.N.shiftl,$_def_Coq.NArith.BinNatDef.N.size_nat,$_def_Coq.NArith.BinNatDef.N.sqrt,$_def_Coq.NArith.BinNatDef.N.sub,$_def_Coq.NArith.BinNatDef.N.succ,$_def_Coq.NArith.BinNatDef.N.succ_double,$_def_Coq.NArith.BinNatDef.N.testbit,$_def_Coq.NArith.BinNatDef.N.testbit_nat,$_def_Coq.NArith.BinNatDef.N.to_nat,$_def_Coq.NArith.Ndec.Nleb,$_def_Coq.NArith.Ndigits.eqf,$_def_Coq.PArith.BinPos.Pos.gt,$_def_Coq.PArith.BinPos.Pos.le,$_def_Coq.PArith.BinPos.Pos.lt,$_def_Coq.PArith.BinPos.Pos.mask2cmp,$_def_Coq.PArith.BinPos.Pos.switch_Eq,$_def_Coq.PArith.BinPosDef.Pos.add,$_def_Coq.PArith.BinPosDef.Pos.compare,$_def_Coq.PArith.BinPosDef.Pos.compare_cont,$_def_Coq.PArith.BinPosDef.Pos.divide,$_def_Coq.PArith.BinPosDef.Pos.eqb,$_def_Coq.PArith.BinPosDef.Pos.leb,$_def_Coq.PArith.BinPosDef.Pos.ltb,$_def_Coq.PArith.BinPosDef.Pos.max,$_def_Coq.PArith.BinPosDef.Pos.min,$_def_Coq.PArith.BinPosDef.Pos.mul,$_def_Coq.PArith.BinPosDef.Pos.of_nat,$_def_Coq.PArith.BinPosDef.Pos.of_succ_nat,$_def_Coq.PArith.BinPosDef.Pos.pred_double,$_def_Coq.PArith.BinPosDef.Pos.size_nat,$_def_Coq.PArith.BinPosDef.Pos.succ,$_def_Coq.PArith.BinPosDef.Pos.to_nat,$_def_Coq.QArith.QArith_base.Qden,$_def_Coq.QArith.QArith_base.Qeq,$_def_Coq.QArith.QArith_base.Qminus,$_def_Coq.QArith.QArith_base.Qnum,$_def_Coq.QArith.QArith_base.inject_Z,$_def_Coq.Reals.Rdefinitions.IZR,$_def_Coq.Reals.Rdefinitions.Rge,$_def_Coq.Reals.Rdefinitions.Rgt,$_def_Coq.Reals.Rdefinitions.Rle,$_def_Coq.Reals.Rdefinitions.Rminus,$_def_Coq.Reals.Rfunctions.R_dist,$_def_Coq.Reals.Rpow_def.pow,$_def_Coq.Relations.Relation_Definitions.relation,$_def_Coq.Relations.Relation_Operators.transp,$_def_Coq.Setoids.Setoid.Setoid_Theory,$_def_Coq.Strings.Ascii.eqb,$_def_Coq.Strings.Byte.to_nat,$_def_Coq.Strings.String.length,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_def_Coq.ZArith.BinInt.Z.Even,$_def_Coq.ZArith.BinInt.Z.b2z,$_def_Coq.ZArith.BinInt.Z.divide,$_def_Coq.ZArith.BinInt.Z.eq,$_def_Coq.ZArith.BinInt.Z.eqf,$_def_Coq.ZArith.BinInt.Z.ge,$_def_Coq.ZArith.BinInt.Z.gt,$_def_Coq.ZArith.BinInt.Z.le,$_def_Coq.ZArith.BinInt.Z.lnot,$_def_Coq.ZArith.BinInt.Z.lt,$_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.eqb,$_def_Coq.ZArith.BinIntDef.Z.even,$_def_Coq.ZArith.BinIntDef.Z.gcd,$_def_Coq.ZArith.BinIntDef.Z.geb,$_def_Coq.ZArith.BinIntDef.Z.gtb,$_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.pow,$_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.shiftr,$_def_Coq.ZArith.BinIntDef.Z.sqrt,$_def_Coq.ZArith.BinIntDef.Z.sub,$_def_Coq.ZArith.BinIntDef.Z.succ,$_def_Coq.ZArith.BinIntDef.Z.to_N,$_def_Coq.ZArith.BinIntDef.Z.to_nat,$_def_Coq.ZArith.BinIntDef.Z.to_pos,$_def_Coq.ZArith.Zbool.Zeq_bool,$_def_Coq.ZArith.Zdiv.Remainder,$_def_Coq.ZArith.Zeven.Zeven,$_def_Coq.ZArith.Zeven.Zodd,$_def_Coq.ZArith.Zlogarithm.Is_power,$_def_Coq.ZArith.Znumtheory.rel_prime,$_def_Coq.ZArith.Zpower.shift_nat,$_def_Coq.micromega.Refl.make_conj,$_def_Coq.micromega.Refl.make_impl,$_def_Coq.micromega.RingMicromega.NFormula,$_def_Coq.micromega.RingMicromega.PolEnv,$_def_Coq.micromega.RingMicromega.eval_op2,$_def_Coq.micromega.RingMicromega.eval_pol,$_def_Coq.micromega.Tauto.clause,$_def_Coq.micromega.Tauto.eval_f,$_def_Coq.micromega.Tauto.eval_tt,$_def_Coq.micromega.ZMicromega.Vars.Facts.MP.Add,$_def_Coq.micromega.ZMicromega.isZ0,$_def_Coq.setoid_ring.Ring_polynom.PEeval,$_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,$_def_Coq.setoid_ring.Ring_theory.pow_N,$_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF,$_discrim_Coq.FSets.FSetPositive.PositiveSet.Leaf$Coq.FSets.FSetPositive.PositiveSet.Node,$_discrim_Coq.Init.Byte.x00$Coq.Init.Byte.x01,$_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT,$_discrim_Coq.Init.Datatypes.Eq$Coq.Init.Datatypes.Lt,$_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S,$_discrim_Coq.Init.Datatypes.Some$Coq.Init.Datatypes.None,$_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.Strings.String.EmptyString$Coq.Strings.String.String,$_discrim_Coq.Structures.OrdersTac.OEQ$Coq.Structures.OrdersTac.OLT,$_discrim_Coq.Vectors.Fin.F1$Coq.Vectors.Fin.FS,$_discrim_Coq.Vectors.VectorDef.nil$Coq.Vectors.VectorDef.cons,$_discrim_Coq.micromega.EnvRing.PEc$Coq.micromega.EnvRing.PEX,$_discrim_Coq.micromega.EnvRing.Pc$Coq.micromega.EnvRing.Pinj,$_discrim_Coq.micromega.RMicromega.C0$Coq.micromega.RMicromega.C1,$_discrim_Coq.micromega.RingMicromega.Equal$Coq.micromega.RingMicromega.NonEqual,$_discrim_Coq.micromega.RingMicromega.OpEq$Coq.micromega.RingMicromega.OpNEq,$_discrim_Coq.micromega.Tauto.TT$Coq.micromega.Tauto.FF,$_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,$_discrim_LF.Basics.true$LF.Basics.false,$_fix_78273_1_add_carry,$_inj_Coq.Bool.Bool.ReflectF,$_inj_Coq.Bool.Bool.ReflectT,$_inj_Coq.FSets.FSetPositive.PositiveSet.Node,$_inj_Coq.Init.Datatypes.CompEqT,$_inj_Coq.Init.Datatypes.CompGtT,$_inj_Coq.Init.Datatypes.CompLtT,$_inj_Coq.Init.Datatypes.None,$_inj_Coq.Init.Datatypes.S,$_inj_Coq.Init.Datatypes.Some,$_inj_Coq.Init.Datatypes.cons,$_inj_Coq.Init.Datatypes.nil,$_inj_Coq.Init.Datatypes.pair,$_inj_Coq.Init.Specif.exist,$_inj_Coq.Init.Specif.exist2,$_inj_Coq.Init.Specif.existT,$_inj_Coq.Init.Specif.existT2,$_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.Strings.Ascii.Ascii,$_inj_Coq.Strings.String.String,$_inj_Coq.Vectors.Fin.F1,$_inj_Coq.Vectors.Fin.FS,$_inj_Coq.Vectors.VectorDef.cons,$_inj_Coq.Vectors.VectorDef.nil,$_inj_Coq.micromega.EnvRing.PEX,$_inj_Coq.micromega.EnvRing.PEadd,$_inj_Coq.micromega.EnvRing.PEc,$_inj_Coq.micromega.EnvRing.PEmul,$_inj_Coq.micromega.EnvRing.PEopp,$_inj_Coq.micromega.EnvRing.PEpow,$_inj_Coq.micromega.EnvRing.PEsub,$_inj_Coq.micromega.EnvRing.PX,$_inj_Coq.micromega.EnvRing.Pc,$_inj_Coq.micromega.EnvRing.Pinj,$_inj_Coq.micromega.RMicromega.CInv,$_inj_Coq.micromega.RMicromega.CMinus,$_inj_Coq.micromega.RMicromega.CMult,$_inj_Coq.micromega.RMicromega.COpp,$_inj_Coq.micromega.RMicromega.CPlus,$_inj_Coq.micromega.RMicromega.CPow,$_inj_Coq.micromega.RMicromega.CQ,$_inj_Coq.micromega.RMicromega.CZ,$_inj_Coq.micromega.RingMicromega.Build_Formula,$_inj_Coq.micromega.Tauto.A,$_inj_Coq.micromega.Tauto.Cj,$_inj_Coq.micromega.Tauto.D,$_inj_Coq.micromega.Tauto.FF,$_inj_Coq.micromega.Tauto.I,$_inj_Coq.micromega.Tauto.N,$_inj_Coq.micromega.Tauto.TT,$_inj_Coq.micromega.Tauto.X,$_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.Arith.Even.even,$_inversion_Coq.Arith.Even.odd,$_inversion_Coq.Bool.Bool.reflect,$_inversion_Coq.FSets.FSetPositive.PositiveSet.tree,$_inversion_Coq.Init.Byte.byte,$_inversion_Coq.Init.Datatypes.CompareSpecT,$_inversion_Coq.Init.Datatypes.bool,$_inversion_Coq.Init.Datatypes.comparison,$_inversion_Coq.Init.Datatypes.list,$_inversion_Coq.Init.Datatypes.nat,$_inversion_Coq.Init.Datatypes.option,$_inversion_Coq.Init.Datatypes.prod,$_inversion_Coq.Init.Datatypes.unit,$_inversion_Coq.Init.Peano.le,$_inversion_Coq.Init.Specif.sig,$_inversion_Coq.Init.Specif.sig2,$_inversion_Coq.Init.Specif.sigT,$_inversion_Coq.Init.Specif.sigT2,$_inversion_Coq.Init.Specif.sumbool,$_inversion_Coq.Lists.List.Add,$_inversion_Coq.Lists.List.Exists,$_inversion_Coq.Lists.List.Forall,$_inversion_Coq.Lists.List.Forall2,$_inversion_Coq.Lists.List.ForallOrdPairs,$_inversion_Coq.Lists.List.NoDup,$_inversion_Coq.Lists.SetoidList.InA,$_inversion_Coq.Lists.SetoidList.NoDupA,$_inversion_Coq.Lists.SetoidList.eqlistA,$_inversion_Coq.Logic.EqdepFacts.eq_dep,$_inversion_Coq.Numbers.BinNums.N,$_inversion_Coq.Numbers.BinNums.Z,$_inversion_Coq.Numbers.BinNums.positive,$_inversion_Coq.PArith.BinPos.Pos.SubMaskSpec,$_inversion_Coq.PArith.BinPosDef.Pos.mask,$_inversion_Coq.QArith.QArith_base.Q,$_inversion_Coq.Relations.Relation_Operators.clos_refl_sym_trans,$_inversion_Coq.Relations.Relation_Operators.clos_refl_sym_trans_1n,$_inversion_Coq.Relations.Relation_Operators.clos_refl_sym_trans_n1,$_inversion_Coq.Relations.Relation_Operators.clos_refl_trans,$_inversion_Coq.Relations.Relation_Operators.clos_refl_trans_1n,$_inversion_Coq.Relations.Relation_Operators.clos_refl_trans_n1,$_inversion_Coq.Relations.Relation_Operators.clos_trans,$_inversion_Coq.Relations.Relation_Operators.clos_trans_1n,$_inversion_Coq.Relations.Relation_Operators.clos_trans_n1,$_inversion_Coq.Sorting.Sorted.HdRel,$_inversion_Coq.Sorting.Sorted.LocallySorted,$_inversion_Coq.Sorting.Sorted.Sorted,$_inversion_Coq.Strings.Ascii.ascii,$_inversion_Coq.Strings.String.string,$_inversion_Coq.Structures.OrdersTac.ord,$_inversion_Coq.Vectors.Fin.t,$_inversion_Coq.Vectors.VectorDef.t,$_inversion_Coq.ZArith.Znumtheory.Zis_gcd,$_inversion_Coq.ZArith.Znumtheory.prime,$_inversion_Coq.micromega.EnvRing.PExpr,$_inversion_Coq.micromega.EnvRing.Pol,$_inversion_Coq.micromega.OrderedRing.SOR,$_inversion_Coq.micromega.RMicromega.Rcst,$_inversion_Coq.micromega.RingMicromega.Formula,$_inversion_Coq.micromega.RingMicromega.Op1,$_inversion_Coq.micromega.RingMicromega.Op2,$_inversion_Coq.micromega.RingMicromega.SORaddon,$_inversion_Coq.micromega.Tauto.GFormula,$_inversion_Coq.setoid_ring.Ring_polynom.Mon,$_inversion_Coq.setoid_ring.Ring_polynom.PExpr,$_inversion_Coq.setoid_ring.Ring_polynom.Pol,$_inversion_Coq.setoid_ring.Ring_theory.ring_theory,$_inversion_LF.Basics.bool,$_lam_113871,$_lam_113902,$_lam_113903,$_lam_124622,$_lam_124630,$_lam_124638,$_lam_124646,$_lam_1363,$_lam_75983,$_lam_75984,$_lam_75986,$_prop_111500,$_prop_118361,$_prop_126724,$_prop_164536,$_prop_164568,$_prop_166141,$_prop_78122,$_prop_96612,$_prop_96613,$_type_100246,$_type_100250,$_type_100285,$_type_100293,$_type_100301,$_type_100371,$_type_101,$_type_101048,$_type_1013,$_type_1024,$_type_102577,$_type_102923,$_type_103269,$_type_103592,$_type_103938,$_type_104,$_type_104284,$_type_104630,$_type_104976,$_type_105322,$_type_105645,$_type_105991,$_type_106337,$_type_106660,$_type_106983,$_type_107329,$_type_107608,$_type_107643,$_type_108014,$_type_108288,$_type_108295,$_type_108321,$_type_108368,$_type_108403,$_type_109012,$_type_110739,$_type_110782,$_type_110821,$_type_110856,$_type_110900,$_type_110917,$_type_110923,$_type_110934,$_type_110952,$_type_110969,$_type_111409,$_type_111447,$_type_111486,$_type_111508,$_type_111512,$_type_113825,$_type_113855,$_type_113873,$_type_113942,$_type_116581,$_type_116586,$_type_116610,$_type_121813,$_type_121840,$_type_121863,$_type_124683,$_type_124778,$_type_126791,$_type_1276,$_type_127967,$_type_1281,$_type_13,$_type_1495,$_type_1500,$_type_1515,$_type_164508,$_type_164534,$_type_165405,$_type_166468,$_type_166602,$_type_166677,$_type_1675,$_type_168314,$_type_168386,$_type_168437,$_type_168915,$_type_168935,$_type_168955,$_type_168973,$_type_168979,$_type_168983,$_type_168992,$_type_1696,$_type_1707,$_type_1724,$_type_1732,$_type_183,$_type_1992,$_type_1999,$_type_2013,$_type_2023,$_type_2029,$_type_2044,$_type_2048,$_type_206,$_type_2065,$_type_211,$_type_2132,$_type_2207,$_type_260,$_type_271,$_type_285,$_type_312,$_type_6,$_type_639,$_type_649,$_type_657,$_type_685,$_type_706,$_type_717,$_type_721,$_type_746,$_type_748,$_type_75030,$_type_75034,$_type_75069,$_type_75071,$_type_75099,$_type_75111,$_type_75114,$_type_75127,$_type_75139,$_type_75159,$_type_755,$_type_75718,$_type_75743,$_type_75849,$_type_76209,$_type_76310,$_type_76314,$_type_76317,$_type_76334,$_type_76351,$_type_76357,$_type_765,$_type_77704,$_type_77726,$_type_77737,$_type_77991,$_type_77995,$_type_78000,$_type_781,$_type_78181,$_type_78303,$_type_78360,$_type_78364,$_type_78395,$_type_78420,$_type_78467,$_type_78568,$_type_78579,$_type_78595,$_type_78598,$_type_78604,$_type_78608,$_type_78836,$_type_78882,$_type_79080,$_type_79094,$_type_79099,$_type_79108,$_type_79389,$_type_8,$_type_801,$_type_806,$_type_80777,$_type_80795,$_type_80803,$_type_80825,$_type_80840,$_type_80842,$_type_80876,$_type_80999,$_type_81078,$_type_81179,$_type_81570,$_type_81622,$_type_81652,$_type_81783,$_type_81793,$_type_81808,$_type_81811,$_type_829,$_type_839,$_type_87987,$_type_89007,$_type_90347,$_type_90371,$_type_90422,$_type_90427,$_type_90432,$_type_90435,$_type_90441,$_type_90675,$_type_90679,$_type_90855,$_type_91368,$_type_92230,$_type_92293,$_type_92356,$_type_92410,$_type_92473,$_type_95372,$_type_95380,$_type_95388,$_type_95422,$_type_96509,$_type_96610,$_type_96649,$_type_96677,$_type_96681,$_type_96794,$_type_96943,$_type_96946,$_type_96948,$_type_97863,$_type_97964,$_type_98065,$_type_98155,$_type_98256,$_type_98357,$_type_98458,$_typeof_Coq.Arith.EqNat.eq_nat,$_typeof_Coq.Arith.PeanoNat.Nat.Even,$_typeof_Coq.Arith.PeanoNat.Nat.Odd,$_typeof_Coq.Arith.PeanoNat.Nat.b2n,$_typeof_Coq.Arith.PeanoNat.Nat.divide,$_typeof_Coq.Arith.PeanoNat.Nat.eqf,$_typeof_Coq.Arith.PeanoNat.Nat.le_alt,$_typeof_Coq.Bool.Bool.Is_true,$_typeof_Coq.Bool.Bool.ReflectF,$_typeof_Coq.Bool.Bool.ReflectT,$_typeof_Coq.Bool.Bool.eqb,$_typeof_Coq.Bool.Bool.leb,$_typeof_Coq.Bool.Bool.reflect,$_typeof_Coq.Bool.Bvector.Bvector,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Equal,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Exists,$_typeof_Coq.FSets.FSetPositive.PositiveSet.For_all,$_typeof_Coq.FSets.FSetPositive.PositiveSet.In,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Leaf,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Node,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Subset,$_typeof_Coq.FSets.FSetPositive.PositiveSet.cardinal,$_typeof_Coq.FSets.FSetPositive.PositiveSet.compare_bool,$_typeof_Coq.FSets.FSetPositive.PositiveSet.elt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.equal,$_typeof_Coq.FSets.FSetPositive.PositiveSet.fold,$_typeof_Coq.FSets.FSetPositive.PositiveSet.is_empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.mem,$_typeof_Coq.FSets.FSetPositive.PositiveSet.rev,$_typeof_Coq.FSets.FSetPositive.PositiveSet.rev_append,$_typeof_Coq.FSets.FSetPositive.PositiveSet.singleton,$_typeof_Coq.FSets.FSetPositive.PositiveSet.t,$_typeof_Coq.FSets.FSetPositive.PositiveSet.tree,$_typeof_Coq.FSets.FSetPositive.PositiveSet.union,$_typeof_Coq.Init.Byte.byte,$_typeof_Coq.Init.Datatypes.CompOpp,$_typeof_Coq.Init.Datatypes.CompSpecT,$_typeof_Coq.Init.Datatypes.CompareSpecT,$_typeof_Coq.Init.Datatypes.Eq,$_typeof_Coq.Init.Datatypes.Gt,$_typeof_Coq.Init.Datatypes.Lt,$_typeof_Coq.Init.Datatypes.None,$_typeof_Coq.Init.Datatypes.O,$_typeof_Coq.Init.Datatypes.S,$_typeof_Coq.Init.Datatypes.Some,$_typeof_Coq.Init.Datatypes.andb,$_typeof_Coq.Init.Datatypes.app,$_typeof_Coq.Init.Datatypes.bool,$_typeof_Coq.Init.Datatypes.comparison,$_typeof_Coq.Init.Datatypes.cons,$_typeof_Coq.Init.Datatypes.false,$_typeof_Coq.Init.Datatypes.fst,$_typeof_Coq.Init.Datatypes.implb,$_typeof_Coq.Init.Datatypes.length,$_typeof_Coq.Init.Datatypes.list,$_typeof_Coq.Init.Datatypes.nat,$_typeof_Coq.Init.Datatypes.negb,$_typeof_Coq.Init.Datatypes.nil,$_typeof_Coq.Init.Datatypes.option,$_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.div,$_typeof_Coq.Init.Nat.div2,$_typeof_Coq.Init.Nat.double,$_typeof_Coq.Init.Nat.eqb,$_typeof_Coq.Init.Nat.even,$_typeof_Coq.Init.Nat.gcd,$_typeof_Coq.Init.Nat.land,$_typeof_Coq.Init.Nat.leb,$_typeof_Coq.Init.Nat.log2,$_typeof_Coq.Init.Nat.ltb,$_typeof_Coq.Init.Nat.max,$_typeof_Coq.Init.Nat.min,$_typeof_Coq.Init.Nat.mul,$_typeof_Coq.Init.Nat.odd,$_typeof_Coq.Init.Nat.pow,$_typeof_Coq.Init.Nat.pred,$_typeof_Coq.Init.Nat.shiftl,$_typeof_Coq.Init.Nat.shiftr,$_typeof_Coq.Init.Nat.sqrt,$_typeof_Coq.Init.Nat.sub,$_typeof_Coq.Init.Nat.testbit,$_typeof_Coq.Init.Peano.ge,$_typeof_Coq.Init.Peano.gt,$_typeof_Coq.Init.Peano.lt,$_typeof_Coq.Init.Specif.exist,$_typeof_Coq.Init.Specif.exist2,$_typeof_Coq.Init.Specif.existT,$_typeof_Coq.Init.Specif.existT2,$_typeof_Coq.Init.Specif.left,$_typeof_Coq.Init.Specif.proj1_sig,$_typeof_Coq.Init.Specif.projT1,$_typeof_Coq.Init.Specif.projT2,$_typeof_Coq.Init.Specif.right,$_typeof_Coq.Init.Specif.sig,$_typeof_Coq.Init.Specif.sig2,$_typeof_Coq.Init.Specif.sigT,$_typeof_Coq.Init.Specif.sigT2,$_typeof_Coq.Init.Specif.sumbool,$_typeof_Coq.Lists.List.In,$_typeof_Coq.Lists.List.existsb,$_typeof_Coq.Lists.List.fold_right,$_typeof_Coq.Lists.List.forallb,$_typeof_Coq.Lists.List.map,$_typeof_Coq.Lists.List.nth,$_typeof_Coq.Lists.List.tl,$_typeof_Coq.Lists.SetoidList.compat_bool,$_typeof_Coq.Lists.SetoidList.equivlistA,$_typeof_Coq.Logic.Decidable.decidable,$_typeof_Coq.NArith.BinNat.N.b2n,$_typeof_Coq.NArith.BinNat.N.divide,$_typeof_Coq.NArith.BinNat.N.eqf,$_typeof_Coq.NArith.BinNat.N.le,$_typeof_Coq.NArith.BinNat.N.le_alt,$_typeof_Coq.NArith.BinNat.N.lt,$_typeof_Coq.NArith.BinNatDef.N.add,$_typeof_Coq.NArith.BinNatDef.N.compare,$_typeof_Coq.NArith.BinNatDef.N.div,$_typeof_Coq.NArith.BinNatDef.N.double,$_typeof_Coq.NArith.BinNatDef.N.eqb,$_typeof_Coq.NArith.BinNatDef.N.even,$_typeof_Coq.NArith.BinNatDef.N.gcd,$_typeof_Coq.NArith.BinNatDef.N.land,$_typeof_Coq.NArith.BinNatDef.N.leb,$_typeof_Coq.NArith.BinNatDef.N.log2,$_typeof_Coq.NArith.BinNatDef.N.lor,$_typeof_Coq.NArith.BinNatDef.N.ltb,$_typeof_Coq.NArith.BinNatDef.N.lxor,$_typeof_Coq.NArith.BinNatDef.N.max,$_typeof_Coq.NArith.BinNatDef.N.min,$_typeof_Coq.NArith.BinNatDef.N.modulo,$_typeof_Coq.NArith.BinNatDef.N.mul,$_typeof_Coq.NArith.BinNatDef.N.odd,$_typeof_Coq.NArith.BinNatDef.N.of_nat,$_typeof_Coq.NArith.BinNatDef.N.pow,$_typeof_Coq.NArith.BinNatDef.N.pred,$_typeof_Coq.NArith.BinNatDef.N.shiftl,$_typeof_Coq.NArith.BinNatDef.N.size_nat,$_typeof_Coq.NArith.BinNatDef.N.sqrt,$_typeof_Coq.NArith.BinNatDef.N.sub,$_typeof_Coq.NArith.BinNatDef.N.succ,$_typeof_Coq.NArith.BinNatDef.N.succ_double,$_typeof_Coq.NArith.BinNatDef.N.testbit,$_typeof_Coq.NArith.BinNatDef.N.testbit_nat,$_typeof_Coq.NArith.BinNatDef.N.to_nat,$_typeof_Coq.NArith.Ndec.Nleb,$_typeof_Coq.NArith.Ndigits.eqf,$_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.gt,$_typeof_Coq.PArith.BinPos.Pos.le,$_typeof_Coq.PArith.BinPos.Pos.lt,$_typeof_Coq.PArith.BinPos.Pos.mask2cmp,$_typeof_Coq.PArith.BinPos.Pos.switch_Eq,$_typeof_Coq.PArith.BinPosDef.Pos.IsNeg,$_typeof_Coq.PArith.BinPosDef.Pos.IsNul,$_typeof_Coq.PArith.BinPosDef.Pos.IsPos,$_typeof_Coq.PArith.BinPosDef.Pos.add,$_typeof_Coq.PArith.BinPosDef.Pos.compare,$_typeof_Coq.PArith.BinPosDef.Pos.compare_cont,$_typeof_Coq.PArith.BinPosDef.Pos.divide,$_typeof_Coq.PArith.BinPosDef.Pos.eqb,$_typeof_Coq.PArith.BinPosDef.Pos.leb,$_typeof_Coq.PArith.BinPosDef.Pos.ltb,$_typeof_Coq.PArith.BinPosDef.Pos.mask,$_typeof_Coq.PArith.BinPosDef.Pos.max,$_typeof_Coq.PArith.BinPosDef.Pos.min,$_typeof_Coq.PArith.BinPosDef.Pos.mul,$_typeof_Coq.PArith.BinPosDef.Pos.of_nat,$_typeof_Coq.PArith.BinPosDef.Pos.of_succ_nat,$_typeof_Coq.PArith.BinPosDef.Pos.pred_double,$_typeof_Coq.PArith.BinPosDef.Pos.size_nat,$_typeof_Coq.PArith.BinPosDef.Pos.succ,$_typeof_Coq.PArith.BinPosDef.Pos.to_nat,$_typeof_Coq.QArith.QArith_base.Q,$_typeof_Coq.QArith.QArith_base.Qden,$_typeof_Coq.QArith.QArith_base.Qeq,$_typeof_Coq.QArith.QArith_base.Qmake,$_typeof_Coq.QArith.QArith_base.Qminus,$_typeof_Coq.QArith.QArith_base.Qnum,$_typeof_Coq.QArith.QArith_base.inject_Z,$_typeof_Coq.Reals.RIneq.Rle_dec,$_typeof_Coq.Reals.Rdefinitions.IZR,$_typeof_Coq.Reals.Rdefinitions.R,$_typeof_Coq.Reals.Rdefinitions.Rge,$_typeof_Coq.Reals.Rdefinitions.Rgt,$_typeof_Coq.Reals.Rdefinitions.Rle,$_typeof_Coq.Reals.Rdefinitions.Rlt,$_typeof_Coq.Reals.Rdefinitions.Rminus,$_typeof_Coq.Reals.Rdefinitions.Rmult,$_typeof_Coq.Reals.Rdefinitions.Ropp,$_typeof_Coq.Reals.Rdefinitions.Rplus,$_typeof_Coq.Reals.Rfunctions.R_dist,$_typeof_Coq.Reals.Rpow_def.pow,$_typeof_Coq.Relations.Relation_Definitions.relation,$_typeof_Coq.Relations.Relation_Operators.transp,$_typeof_Coq.Setoids.Setoid.Setoid_Theory,$_typeof_Coq.Strings.Ascii.ascii,$_typeof_Coq.Strings.Ascii.eqb,$_typeof_Coq.Strings.Byte.to_nat,$_typeof_Coq.Strings.String.EmptyString,$_typeof_Coq.Strings.String.String,$_typeof_Coq.Strings.String.length,$_typeof_Coq.Strings.String.string,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_dec,$_typeof_Coq.Structures.OrdersTac.ord,$_typeof_Coq.Vectors.Fin.F1,$_typeof_Coq.Vectors.Fin.FS,$_typeof_Coq.Vectors.Fin.t,$_typeof_Coq.Vectors.VectorDef.cons,$_typeof_Coq.Vectors.VectorDef.nil,$_typeof_Coq.Vectors.VectorDef.t,$_typeof_Coq.ZArith.BinInt.Z.Even,$_typeof_Coq.ZArith.BinInt.Z.b2z,$_typeof_Coq.ZArith.BinInt.Z.divide,$_typeof_Coq.ZArith.BinInt.Z.eq,$_typeof_Coq.ZArith.BinInt.Z.eqf,$_typeof_Coq.ZArith.BinInt.Z.ge,$_typeof_Coq.ZArith.BinInt.Z.gt,$_typeof_Coq.ZArith.BinInt.Z.le,$_typeof_Coq.ZArith.BinInt.Z.lnot,$_typeof_Coq.ZArith.BinInt.Z.lt,$_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.eqb,$_typeof_Coq.ZArith.BinIntDef.Z.even,$_typeof_Coq.ZArith.BinIntDef.Z.gcd,$_typeof_Coq.ZArith.BinIntDef.Z.geb,$_typeof_Coq.ZArith.BinIntDef.Z.gtb,$_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.pow,$_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.shiftr,$_typeof_Coq.ZArith.BinIntDef.Z.sqrt,$_typeof_Coq.ZArith.BinIntDef.Z.sub,$_typeof_Coq.ZArith.BinIntDef.Z.succ,$_typeof_Coq.ZArith.BinIntDef.Z.to_N,$_typeof_Coq.ZArith.BinIntDef.Z.to_nat,$_typeof_Coq.ZArith.BinIntDef.Z.to_pos,$_typeof_Coq.ZArith.Zbool.Zeq_bool,$_typeof_Coq.ZArith.Zdiv.Remainder,$_typeof_Coq.ZArith.Zeven.Zeven,$_typeof_Coq.ZArith.Zeven.Zodd,$_typeof_Coq.ZArith.Zlogarithm.Is_power,$_typeof_Coq.ZArith.Znumtheory.rel_prime,$_typeof_Coq.ZArith.Zpower.shift_nat,$_typeof_Coq.micromega.EnvRing.PExpr,$_typeof_Coq.micromega.EnvRing.Pc,$_typeof_Coq.micromega.EnvRing.Pol,$_typeof_Coq.micromega.RMicromega.Rcst,$_typeof_Coq.micromega.Refl.make_conj,$_typeof_Coq.micromega.Refl.make_impl,$_typeof_Coq.micromega.RingMicromega.Build_Formula,$_typeof_Coq.micromega.RingMicromega.Equal,$_typeof_Coq.micromega.RingMicromega.Formula,$_typeof_Coq.micromega.RingMicromega.NFormula,$_typeof_Coq.micromega.RingMicromega.NonEqual,$_typeof_Coq.micromega.RingMicromega.NonStrict,$_typeof_Coq.micromega.RingMicromega.Op1,$_typeof_Coq.micromega.RingMicromega.Op2,$_typeof_Coq.micromega.RingMicromega.OpEq,$_typeof_Coq.micromega.RingMicromega.OpGe,$_typeof_Coq.micromega.RingMicromega.OpGt,$_typeof_Coq.micromega.RingMicromega.OpLe,$_typeof_Coq.micromega.RingMicromega.OpLt,$_typeof_Coq.micromega.RingMicromega.OpNEq,$_typeof_Coq.micromega.RingMicromega.PolEnv,$_typeof_Coq.micromega.RingMicromega.Strict,$_typeof_Coq.micromega.RingMicromega.eval_op2,$_typeof_Coq.micromega.RingMicromega.eval_pol,$_typeof_Coq.micromega.Tauto.A,$_typeof_Coq.micromega.Tauto.Cj,$_typeof_Coq.micromega.Tauto.D,$_typeof_Coq.micromega.Tauto.FF,$_typeof_Coq.micromega.Tauto.GFormula,$_typeof_Coq.micromega.Tauto.I,$_typeof_Coq.micromega.Tauto.N,$_typeof_Coq.micromega.Tauto.TT,$_typeof_Coq.micromega.Tauto.X,$_typeof_Coq.micromega.Tauto.clause,$_typeof_Coq.micromega.Tauto.eval_f,$_typeof_Coq.micromega.Tauto.eval_tt,$_typeof_Coq.micromega.ZMicromega.Vars.Facts.MP.Add,$_typeof_Coq.micromega.ZMicromega.isZ0,$_typeof_Coq.setoid_ring.Ring_polynom.Mon,$_typeof_Coq.setoid_ring.Ring_polynom.PEO,$_typeof_Coq.setoid_ring.Ring_polynom.PEX,$_typeof_Coq.setoid_ring.Ring_polynom.PEadd,$_typeof_Coq.setoid_ring.Ring_polynom.PEeval,$_typeof_Coq.setoid_ring.Ring_polynom.PEopp,$_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,$_typeof_Coq.setoid_ring.Ring_theory.pow_N,$_typeof_LF.Basics.bool,$_typeof_LF.Basics.false,$_typeof_LF.Basics.true,Coq.Arith.EqNat.eq_nat_is_eq,Coq.Arith.EqNat.eq_nat_refl,Coq.Arith.Even.even_O,Coq.Arith.Even.even_equiv,Coq.Arith.Even.odd_equiv,Coq.Arith.Gt.gt_S_le,Coq.Arith.Gt.gt_irrefl,Coq.Arith.Gt.gt_le_S,Coq.Arith.Le.le_n_S,Coq.Arith.Lt.le_lt_n_Sm,Coq.Arith.Lt.le_lt_or_eq,Coq.Arith.Lt.lt_le_S,Coq.Arith.Lt.lt_n_S,Coq.Arith.PeanoNat.Nat.Private_NZSqrt.sqrt_le_mono,Coq.Arith.PeanoNat.Nat.Private_OrderTac.IsTotal.le_lteq,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_neq,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_refl,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_sym,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_antisym,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_lt_trans,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.lt_eq,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.lt_irrefl,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.lt_trans,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.neq_eq,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_ge_lt,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_gt_le,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_neq_eq,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_neq,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_refl,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_sym,Coq.Arith.PeanoNat.Nat.Private_Tac.le_antisym,Coq.Arith.PeanoNat.Nat.Private_Tac.le_neq_lt,Coq.Arith.PeanoNat.Nat.Private_Tac.lt_irrefl,Coq.Arith.PeanoNat.Nat.Private_Tac.lt_trans,Coq.Arith.PeanoNat.Nat.Private_Tac.neq_eq,Coq.Arith.PeanoNat.Nat.Private_Tac.neq_sym,Coq.Arith.PeanoNat.Nat.Private_Tac.not_ge_lt,Coq.Arith.PeanoNat.Nat.Private_Tac.not_gt_le,Coq.Arith.PeanoNat.Nat.Private_Tac.not_neq_eq,Coq.Arith.PeanoNat.Nat.add_0_l,Coq.Arith.PeanoNat.Nat.add_0_r,Coq.Arith.PeanoNat.Nat.add_assoc,Coq.Arith.PeanoNat.Nat.add_cancel_l,Coq.Arith.PeanoNat.Nat.add_cancel_r,Coq.Arith.PeanoNat.Nat.add_comm,Coq.Arith.PeanoNat.Nat.add_le_mono,Coq.Arith.PeanoNat.Nat.add_le_mono_l,Coq.Arith.PeanoNat.Nat.add_le_mono_r,Coq.Arith.PeanoNat.Nat.add_lt_mono,Coq.Arith.PeanoNat.Nat.add_lt_mono_l,Coq.Arith.PeanoNat.Nat.add_lt_mono_r,Coq.Arith.PeanoNat.Nat.add_succ_l,Coq.Arith.PeanoNat.Nat.add_wd,Coq.Arith.PeanoNat.Nat.bi_induction,Coq.Arith.PeanoNat.Nat.bits_inj,Coq.Arith.PeanoNat.Nat.central_induction,Coq.Arith.PeanoNat.Nat.compare_lt_iff,Coq.Arith.PeanoNat.Nat.divide_refl,Coq.Arith.PeanoNat.Nat.eq_0_gt_0_cases,Coq.Arith.PeanoNat.Nat.eq_add_0,Coq.Arith.PeanoNat.Nat.eq_decidable,Coq.Arith.PeanoNat.Nat.eq_dne,Coq.Arith.PeanoNat.Nat.eq_equiv,Coq.Arith.PeanoNat.Nat.eq_le_incl,Coq.Arith.PeanoNat.Nat.eq_mul_0,Coq.Arith.PeanoNat.Nat.eq_square_0,Coq.Arith.PeanoNat.Nat.eq_sym_iff,Coq.Arith.PeanoNat.Nat.eqb_eq,Coq.Arith.PeanoNat.Nat.eqf_equiv,Coq.Arith.PeanoNat.Nat.even_spec,Coq.Arith.PeanoNat.Nat.gcd_divide_r,Coq.Arith.PeanoNat.Nat.gcd_eq_0,Coq.Arith.PeanoNat.Nat.le_0_l,Coq.Arith.PeanoNat.Nat.le_0_r,Coq.Arith.PeanoNat.Nat.le_add_r,Coq.Arith.PeanoNat.Nat.le_antisymm,Coq.Arith.PeanoNat.Nat.le_decidable,Coq.Arith.PeanoNat.Nat.le_dne,Coq.Arith.PeanoNat.Nat.le_ge_cases,Coq.Arith.PeanoNat.Nat.le_gt_cases,Coq.Arith.PeanoNat.Nat.le_le_succ_r,Coq.Arith.PeanoNat.Nat.le_lt_trans,Coq.Arith.PeanoNat.Nat.le_lteq,Coq.Arith.PeanoNat.Nat.le_neq,Coq.Arith.PeanoNat.Nat.le_ngt,Coq.Arith.PeanoNat.Nat.le_pred_l,Coq.Arith.PeanoNat.Nat.le_preorder,Coq.Arith.PeanoNat.Nat.le_succ_diag_r,Coq.Arith.PeanoNat.Nat.le_succ_l,Coq.Arith.PeanoNat.Nat.le_trans,Coq.Arith.PeanoNat.Nat.le_wd,Coq.Arith.PeanoNat.Nat.log2_le_mono,Coq.Arith.PeanoNat.Nat.log2_nonneg,Coq.Arith.PeanoNat.Nat.log2_wd,Coq.Arith.PeanoNat.Nat.lt_0_1,Coq.Arith.PeanoNat.Nat.lt_0_succ,Coq.Arith.PeanoNat.Nat.lt_1_2,Coq.Arith.PeanoNat.Nat.lt_asymm,Coq.Arith.PeanoNat.Nat.lt_decidable,Coq.Arith.PeanoNat.Nat.lt_dne,Coq.Arith.PeanoNat.Nat.lt_eq_cases,Coq.Arith.PeanoNat.Nat.lt_ge_cases,Coq.Arith.PeanoNat.Nat.lt_gt_cases,Coq.Arith.PeanoNat.Nat.lt_irrefl,Coq.Arith.PeanoNat.Nat.lt_le_incl,Coq.Arith.PeanoNat.Nat.lt_le_trans,Coq.Arith.PeanoNat.Nat.lt_lt_0,Coq.Arith.PeanoNat.Nat.lt_lt_succ_r,Coq.Arith.PeanoNat.Nat.lt_neq,Coq.Arith.PeanoNat.Nat.lt_nge,Coq.Arith.PeanoNat.Nat.lt_succ_diag_r,Coq.Arith.PeanoNat.Nat.lt_succ_l,Coq.Arith.PeanoNat.Nat.lt_succ_pred,Coq.Arith.PeanoNat.Nat.lt_succ_r,Coq.Arith.PeanoNat.Nat.lt_trichotomy,Coq.Arith.PeanoNat.Nat.lt_wd,Coq.Arith.PeanoNat.Nat.max_l,Coq.Arith.PeanoNat.Nat.max_le_iff,Coq.Arith.PeanoNat.Nat.max_lub_iff,Coq.Arith.PeanoNat.Nat.max_r,Coq.Arith.PeanoNat.Nat.max_spec,Coq.Arith.PeanoNat.Nat.min_glb_iff,Coq.Arith.PeanoNat.Nat.min_l,Coq.Arith.PeanoNat.Nat.min_le_iff,Coq.Arith.PeanoNat.Nat.min_r,Coq.Arith.PeanoNat.Nat.min_spec,Coq.Arith.PeanoNat.Nat.mul_0_l,Coq.Arith.PeanoNat.Nat.mul_0_r,Coq.Arith.PeanoNat.Nat.mul_1_l,Coq.Arith.PeanoNat.Nat.mul_cancel_l,Coq.Arith.PeanoNat.Nat.mul_comm,Coq.Arith.PeanoNat.Nat.mul_le_mono_pos_l,Coq.Arith.PeanoNat.Nat.mul_lt_mono_neg_l,Coq.Arith.PeanoNat.Nat.mul_lt_mono_pos_l,Coq.Arith.PeanoNat.Nat.mul_lt_mono_pos_r,Coq.Arith.PeanoNat.Nat.mul_shuffle3,Coq.Arith.PeanoNat.Nat.mul_wd,Coq.Arith.PeanoNat.Nat.neq_0_lt_0,Coq.Arith.PeanoNat.Nat.neq_succ_0,Coq.Arith.PeanoNat.Nat.nle_gt,Coq.Arith.PeanoNat.Nat.nlt_0_r,Coq.Arith.PeanoNat.Nat.nlt_ge,Coq.Arith.PeanoNat.Nat.odd_spec,Coq.Arith.PeanoNat.Nat.one_succ,Coq.Arith.PeanoNat.Nat.pred_0,Coq.Arith.PeanoNat.Nat.pred_succ,Coq.Arith.PeanoNat.Nat.square_le_mono,Coq.Arith.PeanoNat.Nat.square_lt_mono,Coq.Arith.PeanoNat.Nat.square_nonneg,Coq.Arith.PeanoNat.Nat.sub_0_le,Coq.Arith.PeanoNat.Nat.succ_inj,Coq.Arith.PeanoNat.Nat.succ_inj_wd,Coq.Arith.PeanoNat.Nat.succ_inj_wd_neg,Coq.Arith.PeanoNat.Nat.succ_le_mono,Coq.Arith.PeanoNat.Nat.succ_lt_mono,Coq.Arith.PeanoNat.Nat.succ_wd,Coq.Arith.PeanoNat.Nat.zero_or_succ,Coq.Arith.Plus.le_plus_l,Coq.Bool.Bool.absurd_eq_true,Coq.Bool.Bool.andb_false_iff,Coq.Bool.Bool.andb_lazy_alt,Coq.Bool.Bool.andb_true_iff,Coq.Bool.Bool.diff_false_true,Coq.Bool.Bool.eq_bool_prop_elim,Coq.Bool.Bool.eq_iff_eq_true,Coq.Bool.Bool.eq_true_iff_eq,Coq.Bool.Bool.eqb_true_iff,Coq.Bool.Bool.negb_false_iff,Coq.Bool.Bool.negb_true_iff,Coq.Bool.Bool.not_true_iff_false,Coq.Bool.Bool.orb_false_iff,Coq.Bool.Bool.orb_true_iff,Coq.Bool.Bool.reflect_iff,Coq.FSets.FSetPositive.PositiveSet.empty_1,Coq.Init.Datatypes.CompOpp_iff,Coq.Init.Datatypes.list_ind,Coq.Init.Datatypes.nat_ind,Coq.Init.Datatypes.prod_ind,Coq.Init.Peano.f_equal_nat,Coq.Init.Peano.le_0_n,Coq.Init.Peano.le_S,Coq.Init.Peano.le_S_n,Coq.Init.Peano.le_ind,Coq.Init.Peano.le_n,Coq.Init.Peano.le_n_S,Coq.Init.Peano.plus_n_O,Coq.Init.Specif.proj2_sig,Coq.Lists.List.Forall_forall,Coq.Lists.SetoidList.InA_alt,Coq.Lists.SetoidList.InA_cons,Coq.Lists.SetoidList.InA_cons_hd,Coq.Lists.SetoidList.InA_nil,Coq.Lists.SetoidList.InA_singleton,Coq.Logic.Decidable.contrapositive,Coq.Logic.Decidable.dec_and,Coq.Logic.Decidable.dec_iff,Coq.Logic.Decidable.dec_not_not,Coq.Logic.Decidable.dec_or,Coq.Logic.Decidable.imp_not_l,Coq.Logic.Decidable.imp_simp,Coq.Logic.Decidable.not_and,Coq.Logic.Decidable.not_and_iff,Coq.Logic.Decidable.not_false_iff,Coq.Logic.Decidable.not_iff,Coq.Logic.Decidable.not_imp_iff,Coq.Logic.Decidable.not_imp_rev_iff,Coq.Logic.Decidable.not_not,Coq.Logic.Decidable.not_not_iff,Coq.Logic.Decidable.not_or,Coq.Logic.Decidable.not_or_iff,Coq.Logic.Decidable.not_true_iff,Coq.Logic.Decidable.or_not_l_iff_1,Coq.Logic.Decidable.or_not_l_iff_2,Coq.Logic.Decidable.or_not_r_iff_1,Coq.Logic.Decidable.or_not_r_iff_2,Coq.NArith.BinNat.N.Private_NZSqrt.sqrt_le_mono,Coq.NArith.BinNat.N.Private_OrderTac.IsTotal.le_lteq,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_neq,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_refl,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_sym,Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_antisym,Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_lt_trans,Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_eq,Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_irrefl,Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_trans,Coq.NArith.BinNat.N.Private_OrderTac.Tac.neq_eq,Coq.NArith.BinNat.N.Private_OrderTac.Tac.not_ge_lt,Coq.NArith.BinNat.N.Private_OrderTac.Tac.not_gt_le,Coq.NArith.BinNat.N.Private_OrderTac.Tac.not_neq_eq,Coq.NArith.BinNat.N.Private_Tac.eq_neq,Coq.NArith.BinNat.N.Private_Tac.eq_refl,Coq.NArith.BinNat.N.Private_Tac.eq_sym,Coq.NArith.BinNat.N.Private_Tac.le_antisym,Coq.NArith.BinNat.N.Private_Tac.le_neq_lt,Coq.NArith.BinNat.N.Private_Tac.lt_irrefl,Coq.NArith.BinNat.N.Private_Tac.lt_trans,Coq.NArith.BinNat.N.Private_Tac.neq_eq,Coq.NArith.BinNat.N.Private_Tac.neq_sym,Coq.NArith.BinNat.N.Private_Tac.not_ge_lt,Coq.NArith.BinNat.N.Private_Tac.not_gt_le,Coq.NArith.BinNat.N.Private_Tac.not_neq_eq,Coq.NArith.BinNat.N.add_0_l,Coq.NArith.BinNat.N.add_0_r,Coq.NArith.BinNat.N.add_assoc,Coq.NArith.BinNat.N.add_cancel_l,Coq.NArith.BinNat.N.add_cancel_r,Coq.NArith.BinNat.N.add_comm,Coq.NArith.BinNat.N.add_le_mono,Coq.NArith.BinNat.N.add_le_mono_l,Coq.NArith.BinNat.N.add_le_mono_r,Coq.NArith.BinNat.N.add_lt_mono,Coq.NArith.BinNat.N.add_lt_mono_l,Coq.NArith.BinNat.N.add_lt_mono_r,Coq.NArith.BinNat.N.bi_induction,Coq.NArith.BinNat.N.bits_inj,Coq.NArith.BinNat.N.central_induction,Coq.NArith.BinNat.N.divide_refl,Coq.NArith.BinNat.N.eq_0_gt_0_cases,Coq.NArith.BinNat.N.eq_decidable,Coq.NArith.BinNat.N.eq_dne,Coq.NArith.BinNat.N.eq_equiv,Coq.NArith.BinNat.N.eq_le_incl,Coq.NArith.BinNat.N.eq_mul_0,Coq.NArith.BinNat.N.eq_square_0,Coq.NArith.BinNat.N.eq_sym_iff,Coq.NArith.BinNat.N.eqb_eq,Coq.NArith.BinNat.N.gcd_eq_0,Coq.NArith.BinNat.N.le_0_l,Coq.NArith.BinNat.N.le_add_r,Coq.NArith.BinNat.N.le_ge_cases,Coq.NArith.BinNat.N.le_gt_cases,Coq.NArith.BinNat.N.le_le_succ_r,Coq.NArith.BinNat.N.le_lt_trans,Coq.NArith.BinNat.N.le_lteq,Coq.NArith.BinNat.N.le_ngt,Coq.NArith.BinNat.N.le_preorder,Coq.NArith.BinNat.N.le_succ_diag_r,Coq.NArith.BinNat.N.le_succ_l,Coq.NArith.BinNat.N.le_trans,Coq.NArith.BinNat.N.le_wd,Coq.NArith.BinNat.N.lt_0_1,Coq.NArith.BinNat.N.lt_1_2,Coq.NArith.BinNat.N.lt_asymm,Coq.NArith.BinNat.N.lt_eq_cases,Coq.NArith.BinNat.N.lt_ge_cases,Coq.NArith.BinNat.N.lt_gt_cases,Coq.NArith.BinNat.N.lt_irrefl,Coq.NArith.BinNat.N.lt_le_incl,Coq.NArith.BinNat.N.lt_le_trans,Coq.NArith.BinNat.N.lt_lt_0,Coq.NArith.BinNat.N.lt_neq,Coq.NArith.BinNat.N.lt_nge,Coq.NArith.BinNat.N.lt_succ_diag_r,Coq.NArith.BinNat.N.lt_succ_r,Coq.NArith.BinNat.N.lt_trichotomy,Coq.NArith.BinNat.N.max_le_iff,Coq.NArith.BinNat.N.min_le_iff,Coq.NArith.BinNat.N.mul_0_l,Coq.NArith.BinNat.N.mul_0_r,Coq.NArith.BinNat.N.mul_1_l,Coq.NArith.BinNat.N.mul_cancel_l,Coq.NArith.BinNat.N.mul_comm,Coq.NArith.BinNat.N.mul_le_mono_pos_l,Coq.NArith.BinNat.N.mul_lt_mono_neg_l,Coq.NArith.BinNat.N.mul_lt_mono_pos_l,Coq.NArith.BinNat.N.mul_lt_mono_pos_r,Coq.NArith.BinNat.N.mul_shuffle3,Coq.NArith.BinNat.N.neq_0_lt_0,Coq.NArith.BinNat.N.neq_succ_0,Coq.NArith.BinNat.N.nle_gt,Coq.NArith.BinNat.N.nlt_0_r,Coq.NArith.BinNat.N.nlt_ge,Coq.NArith.BinNat.N.one_succ,Coq.NArith.BinNat.N.pred_succ,Coq.NArith.BinNat.N.square_le_mono,Coq.NArith.BinNat.N.square_lt_mono,Coq.NArith.BinNat.N.succ_inj,Coq.NArith.BinNat.N.succ_inj_wd,Coq.NArith.BinNat.N.succ_inj_wd_neg,Coq.NArith.BinNat.N.succ_le_mono,Coq.NArith.BinNat.N.succ_lt_mono,Coq.NArith.Nnat.N2Nat.inj_iff,Coq.NArith.Nnat.Nat2N.inj_iff,Coq.Numbers.BinNums.positive_ind,Coq.PArith.BinPos.Pos.Private_Tac.eq_neq,Coq.PArith.BinPos.Pos.Private_Tac.eq_refl,Coq.PArith.BinPos.Pos.Private_Tac.eq_sym,Coq.PArith.BinPos.Pos.Private_Tac.le_antisym,Coq.PArith.BinPos.Pos.Private_Tac.lt_irrefl,Coq.PArith.BinPos.Pos.Private_Tac.lt_trans,Coq.PArith.BinPos.Pos.Private_Tac.neq_eq,Coq.PArith.BinPos.Pos.Private_Tac.neq_sym,Coq.PArith.BinPos.Pos.Private_Tac.not_gt_le,Coq.PArith.BinPos.Pos.Private_Tac.not_neq_eq,Coq.PArith.BinPos.Pos.add_cancel_l,Coq.PArith.BinPos.Pos.add_cancel_r,Coq.PArith.BinPos.Pos.add_le_mono_l,Coq.PArith.BinPos.Pos.add_le_mono_r,Coq.PArith.BinPos.Pos.add_lt_mono_l,Coq.PArith.BinPos.Pos.add_lt_mono_r,Coq.PArith.BinPos.Pos.eq_equiv,Coq.PArith.BinPos.Pos.eqb_eq,Coq.PArith.BinPos.Pos.le_lteq,Coq.PArith.BinPos.Pos.lt_eq_cases,Coq.PArith.BinPos.Pos.mul_cancel_l,Coq.PArith.BinPos.Pos.mul_cancel_r,Coq.PArith.BinPos.Pos.mul_le_mono_l,Coq.PArith.BinPos.Pos.mul_lt_mono_l,Coq.PArith.BinPos.Pos.mul_lt_mono_r,Coq.PArith.BinPos.Pos.succ_le_mono,Coq.PArith.Pnat.Pos2Nat.inj_iff,Coq.QArith.QArith_base.Q_Setoid,Coq.QArith.QArith_base.Qle_refl,Coq.QArith.QArith_base.Qmult_comm,Coq.QArith.QArith_base.Qplus_comm,Coq.Reals.RIneq.Req_ge,Coq.Reals.RIneq.Req_ge_sym,Coq.Reals.RIneq.Req_le,Coq.Reals.RIneq.Req_le_sym,Coq.Reals.RIneq.Rge_ge_eq,Coq.Reals.RIneq.Rge_le,Coq.Reals.RIneq.Rle_antisym,Coq.Reals.RIneq.Rle_ge,Coq.Reals.RIneq.Rle_le_eq,Coq.Reals.RIneq.Rle_lt_trans,Coq.Reals.RIneq.Rle_trans,Coq.Reals.RIneq.Rlt_le,Coq.Reals.RIneq.Rnot_le_lt,Coq.Reals.Raxioms.Rlt_trans,Coq.Sorting.Sorted.HdRel_nil,Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_refl,Coq.ZArith.BinInt.Pos2Z.inj_iff,Coq.ZArith.BinInt.Pos2Z.inj_neg_iff,Coq.ZArith.BinInt.Pos2Z.inj_pos_iff,Coq.ZArith.BinInt.Z.Private_OrderTac.IsTotal.le_lteq,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.le_antisym,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.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_neq,Coq.ZArith.BinInt.Z.Private_Tac.eq_refl,Coq.ZArith.BinInt.Z.Private_Tac.eq_sym,Coq.ZArith.BinInt.Z.Private_Tac.le_antisym,Coq.ZArith.BinInt.Z.Private_Tac.le_neq_lt,Coq.ZArith.BinInt.Z.Private_Tac.lt_irrefl,Coq.ZArith.BinInt.Z.Private_Tac.lt_trans,Coq.ZArith.BinInt.Z.Private_Tac.neq_eq,Coq.ZArith.BinInt.Z.Private_Tac.neq_sym,Coq.ZArith.BinInt.Z.Private_Tac.not_ge_lt,Coq.ZArith.BinInt.Z.Private_Tac.not_gt_le,Coq.ZArith.BinInt.Z.Private_Tac.not_neq_eq,Coq.ZArith.BinInt.Z.abs_0_iff,Coq.ZArith.BinInt.Z.abs_eq,Coq.ZArith.BinInt.Z.abs_nonneg,Coq.ZArith.BinInt.Z.add_0_l,Coq.ZArith.BinInt.Z.add_0_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_mono_l,Coq.ZArith.BinInt.Z.add_le_mono_r,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_move_l,Coq.ZArith.BinInt.Z.add_move_r,Coq.ZArith.BinInt.Z.add_nonneg_nonneg,Coq.ZArith.BinInt.Z.add_opp_r,Coq.ZArith.BinInt.Z.bi_induction,Coq.ZArith.BinInt.Z.bits_0,Coq.ZArith.BinInt.Z.bits_inj',Coq.ZArith.BinInt.Z.central_induction,Coq.ZArith.BinInt.Z.compare_eq_iff,Coq.ZArith.BinInt.Z.divide_0_r,Coq.ZArith.BinInt.Z.divide_1_l,Coq.ZArith.BinInt.Z.divide_abs_l,Coq.ZArith.BinInt.Z.divide_abs_r,Coq.ZArith.BinInt.Z.divide_factor_l,Coq.ZArith.BinInt.Z.divide_factor_r,Coq.ZArith.BinInt.Z.divide_opp_l,Coq.ZArith.BinInt.Z.divide_opp_r,Coq.ZArith.BinInt.Z.divide_refl,Coq.ZArith.BinInt.Z.eq_decidable,Coq.ZArith.BinInt.Z.eq_dne,Coq.ZArith.BinInt.Z.eq_equiv,Coq.ZArith.BinInt.Z.eq_mul_0,Coq.ZArith.BinInt.Z.eq_opp_l,Coq.ZArith.BinInt.Z.eq_opp_r,Coq.ZArith.BinInt.Z.eq_square_0,Coq.ZArith.BinInt.Z.eq_sym_iff,Coq.ZArith.BinInt.Z.eqb_eq,Coq.ZArith.BinInt.Z.gcd_divide_iff,Coq.ZArith.BinInt.Z.gcd_divide_l,Coq.ZArith.BinInt.Z.gcd_divide_r,Coq.ZArith.BinInt.Z.gcd_eq_0,Coq.ZArith.BinInt.Z.gcd_nonneg,Coq.ZArith.BinInt.Z.ge_le_iff,Coq.ZArith.BinInt.Z.gt_lt_iff,Coq.ZArith.BinInt.Z.le_0_sub,Coq.ZArith.BinInt.Z.le_decidable,Coq.ZArith.BinInt.Z.le_dne,Coq.ZArith.BinInt.Z.le_ge_cases,Coq.ZArith.BinInt.Z.le_gt_cases,Coq.ZArith.BinInt.Z.le_le_succ_r,Coq.ZArith.BinInt.Z.le_lt_trans,Coq.ZArith.BinInt.Z.le_lteq,Coq.ZArith.BinInt.Z.le_ngt,Coq.ZArith.BinInt.Z.le_preorder,Coq.ZArith.BinInt.Z.le_refl,Coq.ZArith.BinInt.Z.le_sub_0,Coq.ZArith.BinInt.Z.le_sub_le_add,Coq.ZArith.BinInt.Z.le_sub_nonneg,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.log2_le_mono,Coq.ZArith.BinInt.Z.log2_nonneg,Coq.ZArith.BinInt.Z.log2_wd,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_asymm,Coq.ZArith.BinInt.Z.lt_decidable,Coq.ZArith.BinInt.Z.lt_dne,Coq.ZArith.BinInt.Z.lt_eq_cases,Coq.ZArith.BinInt.Z.lt_ge_cases,Coq.ZArith.BinInt.Z.lt_gt_cases,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_mul_0,Coq.ZArith.BinInt.Z.lt_neq,Coq.ZArith.BinInt.Z.lt_nge,Coq.ZArith.BinInt.Z.lt_sub_0,Coq.ZArith.BinInt.Z.lt_sub_lt_add_r,Coq.ZArith.BinInt.Z.lt_sub_pos,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.max_l,Coq.ZArith.BinInt.Z.max_le_iff,Coq.ZArith.BinInt.Z.max_lub_iff,Coq.ZArith.BinInt.Z.max_r,Coq.ZArith.BinInt.Z.max_spec,Coq.ZArith.BinInt.Z.min_glb_iff,Coq.ZArith.BinInt.Z.min_l,Coq.ZArith.BinInt.Z.min_le_iff,Coq.ZArith.BinInt.Z.min_r,Coq.ZArith.BinInt.Z.min_spec,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_cancel_l,Coq.ZArith.BinInt.Z.mul_cancel_r,Coq.ZArith.BinInt.Z.mul_comm,Coq.ZArith.BinInt.Z.mul_eq_0,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_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_pos_l,Coq.ZArith.BinInt.Z.mul_lt_mono_pos_r,Coq.ZArith.BinInt.Z.mul_opp_l,Coq.ZArith.BinInt.Z.mul_pos_cancel_l,Coq.ZArith.BinInt.Z.mul_pos_cancel_r,Coq.ZArith.BinInt.Z.mul_pos_pos,Coq.ZArith.BinInt.Z.mul_shuffle1,Coq.ZArith.BinInt.Z.mul_shuffle3,Coq.ZArith.BinInt.Z.neq_mul_0,Coq.ZArith.BinInt.Z.nle_gt,Coq.ZArith.BinInt.Z.nlt_ge,Coq.ZArith.BinInt.Z.one_succ,Coq.ZArith.BinInt.Z.opp_0,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.peano_ind,Coq.ZArith.BinInt.Z.pow_neg_r,Coq.ZArith.BinInt.Z.pred_inj_wd,Coq.ZArith.BinInt.Z.pred_le_mono,Coq.ZArith.BinInt.Z.pred_lt_mono,Coq.ZArith.BinInt.Z.pred_succ,Coq.ZArith.BinInt.Z.sgn_null_iff,Coq.ZArith.BinInt.Z.sqrt_le_mono,Coq.ZArith.BinInt.Z.square_nonneg,Coq.ZArith.BinInt.Z.sub_0_r,Coq.ZArith.BinInt.Z.sub_cancel_l,Coq.ZArith.BinInt.Z.sub_cancel_r,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_lt_mono_l,Coq.ZArith.BinInt.Z.sub_lt_mono_r,Coq.ZArith.BinInt.Z.sub_move_0_r,Coq.ZArith.BinInt.Z.sub_move_r,Coq.ZArith.BinInt.Z.sub_simpl_r,Coq.ZArith.BinInt.Z.succ_inj,Coq.ZArith.BinInt.Z.succ_inj_wd,Coq.ZArith.BinInt.Z.succ_inj_wd_neg,Coq.ZArith.BinInt.Z.succ_le_mono,Coq.ZArith.BinInt.Z.succ_lt_mono,Coq.ZArith.BinInt.Z.succ_pred,Coq.ZArith.BinInt.Zpos_eq_iff,Coq.ZArith.Znat.N2Z.inj_iff,Coq.ZArith.Znat.Nat2Z.inj_iff,Coq.ZArith.Znumtheory.Zis_gcd_intro,Coq.ZArith.Zorder.Znot_ge_lt,Coq.ZArith.Zorder.Znot_gt_le,Coq.ZArith.Zorder.Znot_le_gt,Coq.ZArith.Zorder.Znot_lt_ge,Coq.ZArith.Zorder.dec_Zge,Coq.ZArith.Zorder.dec_Zgt,Coq.ZArith.auxiliary.Zegal_left,Coq.ZArith.auxiliary.Zge_left,Coq.ZArith.auxiliary.Zle_left,Coq.micromega.OrderedRing.Req_dne,Coq.micromega.OrderedRing.Req_em,Coq.micromega.OrderedRing.Rle_gt_cases,Coq.micromega.OrderedRing.Rle_le_minus,Coq.micromega.OrderedRing.Rle_lt_eq,Coq.micromega.OrderedRing.Rle_lt_trans,Coq.micromega.OrderedRing.Rle_ngt,Coq.micromega.OrderedRing.Rle_refl,Coq.micromega.OrderedRing.Rlt_le_neq,Coq.micromega.OrderedRing.Rlt_le_trans,Coq.micromega.OrderedRing.Rlt_lt_minus,Coq.micromega.OrderedRing.Rlt_neq,Coq.micromega.OrderedRing.Rlt_nge,Coq.micromega.OrderedRing.Rminus_eq_0,Coq.micromega.OrderedRing.Rneq_symm,Coq.micromega.OrderedRing.Ropp_lt_mono,Coq.micromega.OrderedRing.Ropp_neg_pos,Coq.micromega.OrderedRing.Ropp_pos_neg,Coq.micromega.OrderedRing.Rplus_0_l,Coq.micromega.OrderedRing.Rplus_cancel_l,Coq.micromega.OrderedRing.Rplus_comm,Coq.micromega.OrderedRing.Rplus_le_mono_l,Coq.micromega.OrderedRing.Rplus_le_mono_r,Coq.micromega.OrderedRing.Rplus_lt_mono_l,Coq.micromega.OrderedRing.Rplus_lt_mono_r,Coq.micromega.OrderedRing.SORle_antisymm,Coq.micromega.OrderedRing.SORle_refl,Coq.micromega.OrderedRing.SORle_trans,Coq.micromega.OrderedRing.SORle_wd,Coq.micromega.OrderedRing.SORlt_le_neq,Coq.micromega.OrderedRing.SORlt_trichotomy,Coq.micromega.OrderedRing.SORlt_wd,Coq.micromega.OrderedRing.SORneq_0_1,Coq.micromega.OrderedRing.SORopp_wd,Coq.micromega.OrderedRing.SORplus_le_mono_l,Coq.micromega.OrderedRing.SORplus_wd,Coq.micromega.OrderedRing.SORrt,Coq.micromega.OrderedRing.SORsetoid,Coq.micromega.OrderedRing.SORtimes_pos_pos,Coq.micromega.OrderedRing.SORtimes_wd,Coq.micromega.OrderedRing.mk_SOR_theory,Coq.micromega.OrderedRing.rle_morph,Coq.micromega.OrderedRing.rle_morph_Proper,Coq.micromega.OrderedRing.rlt_morph,Coq.micromega.OrderedRing.rlt_morph_Proper,Coq.micromega.OrderedRing.rminus_morph_Proper,Coq.micromega.OrderedRing.ropp_morph_Proper,Coq.micromega.OrderedRing.rplus_morph_Proper,Coq.micromega.OrderedRing.sor_setoid,Coq.micromega.OrderedRing.sor_setoid_Reflexive,Coq.micromega.OrderedRing.sor_setoid_Transitive,Coq.micromega.RingMicromega.rle_morph,Coq.micromega.RingMicromega.rle_morph_Proper,Coq.micromega.RingMicromega.rlt_morph,Coq.micromega.RingMicromega.rlt_morph_Proper,Coq.micromega.Tauto.eval_f_morph,Coq.micromega.ZCoeff.rle_morph,Coq.micromega.ZCoeff.rle_morph_Proper,Coq.micromega.ZCoeff.rlt_morph,Coq.micromega.ZCoeff.rlt_morph_Proper,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.E_ST,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.In_eq_iff,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.add_iff,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.empty_iff,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.inter_iff,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.union_iff,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.eq_refl_iff,Coq.omega.OmegaLemmas.OMEGA2,Coq.omega.OmegaLemmas.fast_Zplus_comm,Coq.omega.OmegaLemmas.new_var,Logic.iff_sym,$adef_Coq.FSets.FSetPositive.PositiveSet.xfold_$a5,$adef_Coq.Arith.PeanoNat.Nat.eqf_$a2,$adef_Coq.ZArith.BinInt.Z.Even_$a1,$adef_Coq.NArith.Ndigits.eqf_$a2,$adef_Coq.Reals.Rdefinitions.IZR_$a1,$adef_$_prop_118361_$a2,$adef_Coq.Init.Datatypes.None_$a1,$adef_Coq.ZArith.BinIntDef.Z.to_nat_$a1,$adef_Coq.NArith.BinNat.N.lt_$a2,$adef_Coq.Vectors.VectorDef.cons_$a4,$adef_Coq.ZArith.BinIntDef.Z.of_N_$a1,$adef_Coq.Relations.Relation_Operators.clos_refl_sym_trans_$a4,$adef_Coq.ZArith.BinIntDef.Z.modulo_$a2,$adef_Coq.Reals.Rfunctions.R_dist_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.rev_$a1,$adef_Coq.PArith.BinPosDef.Pos.of_nat_$a1,$adef_Coq.Lists.List.Exists_$a3,$adef_Coq.setoid_ring.Ring_polynom.mk_monpol_list_$a10,$adef_Coq.micromega.RingMicromega.eval_pol_$a5,$adef_Coq.setoid_ring.Ring_polynom.PEc_$a2,$adef_Coq.Init.Datatypes.implb_$a2,$adef_Coq.micromega.EnvRing.Pol_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.inter_$a2,$adef_Coq.ZArith.BinIntDef.Z.log2_$a1,$adef_Coq.micromega.Tauto.Cj_$a6,$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.micromega.RMicromega.CMult_$a2,$adef_Coq.Init.Nat.log2_iter_$a4,$adef_$_prop_164568_$a2,$adef_Coq.Init.Nat.even_$a1,$adef_Coq.Sorting.Sorted.LocallySorted_$a3,$adef_Coq.setoid_ring.Ring_polynom.vmon_$a2,$adef_Coq.NArith.BinNatDef.N.div_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.compare_bool_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.Exists_$a2,$adef_Coq.setoid_ring.BinList.nth_$a4,$adef_Coq.setoid_ring.Ring_polynom.Pol_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.mem_$a2,$adef_Coq.Relations.Relation_Operators.clos_refl_sym_trans_n1_$a4,$adef_Coq.Reals.Rdefinitions.IPR_$a1,$adef_Coq.Arith.PeanoNat.Nat.le_alt_$a2,$adef_Coq.micromega.Env.Env_$a1,$adef_Coq.Init.Datatypes.CompareSpecT_$a4,$adef_Coq.ZArith.BinIntDef.Z.pred_$a1,$adef_Coq.Init.Nat.compare_$a2,$adef_Coq.Init.Specif.projT2_$a3,$adef_Coq.micromega.Tauto.eval_f_$a7,$adef_Coq.Init.Datatypes.app_$a3,$adef_Coq.Init.Specif.existT_$a4,$adef_Coq.FSets.FSetPositive.PositiveSet.singleton_$a1,$adef_Coq.Init.Specif.sig_$a2,$adef_Coq.NArith.BinNatDef.N.sqrt_$a1,$adef_Coq.ZArith.BinIntDef.Z.leb_$a2,$adef_Coq.Relations.Relation_Operators.transp_$a4,$adef_Coq.PArith.BinPosDef.Pos.pred_double_$a1,$adef_Coq.ZArith.BinIntDef.Z.mul_$a2,$adef_$_lam_124622_$a4,$adef_Coq.ZArith.BinIntDef.Z.sqrt_$a1,$adef_Coq.PArith.BinPosDef.Pos.divide_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.Equal_$a2,$adef_Coq.micromega.RingMicromega.Build_Formula_$a4,$adef_Coq.Init.Specif.sumbool_$a2,$adef_$_case_Coq.Init.Datatypes.bool$164137_$a14,$adef_Coq.Init.Specif.proj1_sig_$a3,$adef_Coq.Init.Nat.div_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEsub_$a3,$adef_Coq.Lists.List.existsb_$a3,$adef_Coq.Init.Nat.max_$a2,$adef_Coq.PArith.BinPosDef.Pos.pred_N_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.cardinal_$a1,$adef_Coq.Init.Datatypes.option_$a1,$adef_Coq.Relations.Relation_Definitions.relation_$a1,$adef_Coq.ZArith.BinIntDef.Z.eqb_$a2,$adef_Coq.NArith.BinNatDef.N.sub_$a2,$adef_Coq.setoid_ring.Ring_polynom.Peq_$a4,$adef_Coq.Lists.List.forallb_$a3,$adef_Coq.Vectors.VectorDef.t_$a2,$adef_Coq.setoid_ring.Ring_polynom.PExpr_$a1,$adef_Coq.Init.Datatypes.orb_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.rev_append_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_morph_$a17,$adef_Coq.Init.Datatypes.CompOpp_$a1,$adef_Coq.micromega.EnvRing.PEopp_$a2,$adef_Coq.micromega.RingMicromega.SORaddon_$a22,$adef_Coq.micromega.RingMicromega.PolEnv_$a1,$adef_Coq.NArith.BinNat.N.b2n_$a1,$adef_Coq.Reals.Rdefinitions.Rle_$a2,$adef_$_lam_113903_$a1,$adef_Coq.NArith.BinNatDef.N.testbit_$a1,$adef_Coq.PArith.BinPosDef.Pos.compare_cont_$a3,$adef_$_lam_113871_$a1,$adef_Coq.Logic.EqdepFacts.eq_dep_$a6,$adef_Coq.QArith.QArith_base.Qle_$a2,$adef_Coq.Init.Nat.eqb_$a2,$adef_Coq.Sorting.Sorted.HdRel_$a4,$adef_Coq.NArith.BinNat.N.divide_$a2,$adef_Coq.Strings.String.length_$a1,$adef_Coq.PArith.BinPosDef.Pos.testbit_nat_$a1,$adef_$_case_Coq.Init.Datatypes.bool$164282_$a4,$adef_Coq.ZArith.BinIntDef.Z.to_N_$a1,$adef_Coq.ZArith.BinInt.Z.b2z_$a1,$adef_Coq.Lists.List.Forall2_$a5,$adef_Coq.Init.Datatypes.nil_$a1,$adef_Coq.NArith.BinNatDef.N.max_$a2,$adef_Coq.Reals.Rdefinitions.Rge_$a2,$adef_Coq.Init.Datatypes.CompGtT_$a3,$adef_Coq.Reals.Rdefinitions.Rmult_$a2,$adef_Coq.Init.Datatypes.CompareSpecT_$a3,$adef_Coq.micromega.Tauto.GFormula_$a4,$adef_Coq.Numbers.BinNums.Npos_$a1,$adef_Coq.Numbers.BinNums.xI_$a1,$adef_$_case_Coq.Init.Datatypes.bool$166575_$a2,$adef_Coq.ZArith.Zeven.Zodd_$a1,$adef_$_lam_124638_$a4,$adef_Coq.ZArith.BinIntDef.Z.geb_$a2,$adef_Coq.ZArith.BinIntDef.Z.ltb_$a2,$adef_Coq.micromega.RMicromega.CPow_$a2,$adef_Coq.ZArith.BinIntDef.Z.abs_nat_$a1,$adef_Coq.micromega.RMicromega.CPlus_$a2,$adef_Coq.ZArith.BinIntDef.Z.to_pos_$a1,$adef_Coq.Init.Nat.div2_$a1,$adef_Coq.Init.Datatypes.negb_$a1,$adef_Coq.Init.Nat.log2_$a1,$adef_Coq.micromega.RMicromega.COpp_$a1,$adef_Coq.Init.Nat.testbit_$a2,$adef_Coq.NArith.Ndec.Nleb_$a2,$adef_Coq.Reals.Rdefinitions.Ropp_$a1,$adef_Coq.Strings.Byte.to_nat_$a1,$adef_Coq.setoid_ring.Ring_polynom.PEeval_$a14,$adef_Coq.Init.Datatypes.nat_rect_$a3,$adef_Coq.Arith.Even.odd_$a1,$adef_Coq.Lists.List.ForallOrdPairs_$a3,$adef_Coq.ZArith.BinIntDef.Z.succ_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.add_$a2,$adef_Coq.Relations.Relation_Operators.clos_trans_1n_$a4,$adef_Coq.Init.Nat.add_$a2,$adef_Coq.Init.Specif.sigT2_$a3,$adef_Coq.Classes.Morphisms.Proper_$a3,$adef_Coq.Reals.Rdefinitions.Rminus_$a2,$adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2,$adef_Coq.PArith.BinPos.Pos.gt_$a2,$adef_Coq.Init.Nat.ltb_$a2,$adef_Coq.Init.Specif.right_$a2,$adef_Coq.setoid_ring.Ring_theory.power_theory_$a7,$adef_Coq.NArith.BinNatDef.N.size_nat_$a1,$adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3,$adef_Coq.Reals.Rdefinitions.Rplus_$a2,$adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2,$adef_Coq.Lists.List.Add_$a4,$adef_Coq.micromega.RMicromega.CMinus_$a2,$adef_$_lam_124622_$a2,$adef_Coq.PArith.BinPosDef.Pos.sqrt_$a1,$adef_Coq.ZArith.BinIntDef.Z.odd_$a1,$adef_Coq.Init.Datatypes.S_$a1,$adef_$_case_Coq.Init.Datatypes.bool$168311_$a2,$adef_Coq.Strings.Ascii.Ascii_$a8,$adef_Coq.micromega.EnvRing.PEpow_$a3,$adef_Coq.setoid_ring.Ring_polynom.zmon_$a2,$adef_Coq.ZArith.BinIntDef.Z.add_$a2,$adef_Coq.micromega.RingMicromega.Formula_$a1,$adef_Coq.Lists.SetoidList.InA_$a4,$adef_$_lam_113902_$a1,$adef_Coq.Reals.Rdefinitions.Rlt_$a2,$adef_Coq.ZArith.BinIntDef.Z.sub_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEopp_$a2,$adef_Coq.Init.Nat.modulo_$a2,$adef_Coq.setoid_ring.Ring_theory.pow_pos_$a4,$adef_Coq.Init.Nat.pow_$a2,$adef_Coq.micromega.Tauto.I_$a7,$adef_Coq.micromega.Refl.make_conj_$a3,$adef_Coq.PArith.BinPos.Pos.switch_Eq_$a2,$adef_Coq.ZArith.BinIntDef.Z.even_$a1,$adef_Coq.ZArith.BinInt.Z.gt_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEO_$a1,$adef_Coq.PArith.BinPosDef.Pos.land_$a2,$adef_Coq.Numbers.BinNums.xO_$a1,$adef_Coq.ZArith.Zdiv.Remainder_$a2,$adef_Coq.micromega.EnvRing.Pphi_$a5,$adef_Coq.setoid_ring.Ring_theory.pow_N_$a5,$adef_Coq.NArith.BinNatDef.N.of_nat_$a1,$adef_Coq.ZArith.BinInt.Z.ge_$a2,$adef_Coq.QArith.QArith_base.Qeq_$a2,$adef_Coq.ZArith.Zbool.Zeq_bool_$a2,$adef_$_case_Coq.Init.Datatypes.bool$164198_$a12,$adef_Coq.micromega.RMicromega.CQ_$a1,$adef_Coq.QArith.QArith_base.Qmake_$a2,$adef_Coq.micromega.EnvRing.PEc_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEX_$a2,$adef_Coq.NArith.BinNatDef.N.pred_$a1,$adef_Coq.micromega.OrderedRing.SOR_$a10,$adef_Coq.Relations.Relation_Operators.clos_refl_trans_$a4,$adef_Coq.Init.Nat.sqrt_$a1,$adef_Coq.NArith.BinNatDef.N.min_$a2,$adef_Coq.ZArith.Znumtheory.Zis_gcd_$a3,$adef_Coq.PArith.BinPosDef.Pos.iter_op_$a4,$adef_Coq.PArith.BinPosDef.Pos.size_$a1,$adef_Coq.Init.Datatypes.CompSpecT_$a5,$adef_Coq.setoid_ring.Ring_polynom.norm_aux_$a9,$adef_Coq.Relations.Relation_Operators.clos_trans_$a4,$adef_Coq.Relations.Relation_Operators.clos_refl_sym_trans_1n_$a4,$adef_Coq.Vectors.Fin.t_$a1,$adef_$_lam_75986_$a1,$adef_Coq.Lists.List.In_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.Empty_$a1,$adef_Coq.Init.Datatypes.andb_$a2,$adef_Coq.Init.Peano.lt_$a2,$adef_Coq.NArith.BinNatDef.N.land_$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.FSets.FSetPositive.PositiveSet.Node_$a3,$adef_Coq.Arith.PeanoNat.Nat.divide_$a2,$adef_$_lam_75984_$a1,$adef_$_let_11_subst_l_1291_$a10,$adef_Coq.Classes.RelationClasses.Equivalence_$a2,$adef_Coq.Arith.Even.even_$a1,$adef_Coq.micromega.Tauto.TT_$a4,$adef_Coq.Logic.Decidable.decidable_$a1,$adef_Coq.Relations.Relation_Operators.clos_trans_n1_$a4,$adef_Coq.micromega.EnvRing.PEmul_$a3,$adef_Coq.Init.Datatypes.snd_$a3,$adef_Coq.ZArith.BinInt.Z.eqf_$a2,$adef_Coq.QArith.QArith_base.Qmult_$a2,$adef_Coq.PArith.BinPos.Pos.lt_$a2,$adef_Coq.ZArith.BinIntDef.Z.gcd_$a2,$adef_$_lam_1363_$a12,$adef_Coq.NArith.BinNatDef.N.testbit_$a2,$adef_Coq.PArith.BinPosDef.Pos.to_nat_$a1,$adef_$_lam_1363_$a11,$adef_Coq.ZArith.BinIntDef.Z.abs_N_$a1,$adef_Coq.PArith.BinPosDef.Pos.size_nat_$a1,$adef_Coq.Init.Datatypes.CompLtT_$a3,$adef_Coq.Lists.List.nth_$a4,$adef_Coq.ZArith.Znumtheory.prime_$a1,$adef_Coq.PArith.BinPos.Pos.mask2cmp_$a1,$adef_Coq.micromega.RingMicromega.eval_op2_$a5,$adef_$_case_Coq.Init.Datatypes.bool$164277_$a6,$adef_Coq.Vectors.Fin.F1_$a1,$adef_Coq.QArith.QArith_base.Qnum_$a1,$adef_Coq.setoid_ring.Ring_polynom.PNSubstL_$a11,$adef_Coq.NArith.BinNatDef.N.succ_double_$a1,$adef_Coq.PArith.BinPosDef.Pos.succ_$a1,$adef_Coq.ZArith.BinIntDef.Z.shiftr_$a2,$adef_Coq.micromega.Tauto.D_$a6,$adef_Coq.Init.Datatypes.prod_$a2,$adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a12,$adef_Coq.PArith.BinPosDef.Pos.lor_$a2,$adef_Coq.NArith.BinNatDef.N.shiftl_$a2,$adef_Coq.ZArith.BinIntDef.Z.compare_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_theory_$a8,$adef_Coq.QArith.QArith_base.Qden_$a1,$adef_Coq.Init.Nat.shiftl_$a1,$adef_Coq.micromega.Tauto.eval_tt_$a6,$adef_Coq.ZArith.BinIntDef.Z.testbit_$a2,$adef_Coq.NArith.BinNatDef.N.gcd_$a2,$adef_Coq.Vectors.VectorDef.t_$a1,$adef_Coq.Bool.Bool.eqb_$a2,$adef_Coq.NArith.BinNatDef.N.div_eucl_$a2,$adef_Coq.micromega.RMicromega.CZ_$a1,$adef_Coq.ZArith.BinInt.Z.lt_$a2,$adef_Coq.Init.Nat.gcd_$a2,$adef_Coq.micromega.ZMicromega.isZ0_$a1,$adef_Coq.Arith.PeanoNat.Nat.b2n_$a1,$adef_Coq.PArith.BinPosDef.Pos.eqb_$a2,$adef_Coq.ZArith.Zlogarithm.Is_power_$a1,$adef_Coq.ZArith.BinIntDef.Z.opp_$a1,$adef_Coq.QArith.QArith_base.inject_Z_$a1,$adef_$_lam_75983_$a1,$adef_Coq.Numbers.BinNums.Zneg_$a1,$adef_Coq.QArith.QArith_base.Qminus_$a2,$adef_Coq.Reals.Rdefinitions.Rgt_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3,$adef_Coq.NArith.BinNatDef.N.to_nat_$a1,$adef_Coq.Classes.RelationClasses.Transitive_$a2,$adef_Coq.ZArith.Zeven.Zeven_$a1,$adef_$_prop_78122_$a2,$adef_Coq.Bool.Bool.reflect_$a2,$adef_Coq.NArith.BinNatDef.N.pow_$a2,$adef_Coq.setoid_ring.Ring_polynom.PX_$a4,$adef_Coq.NArith.BinNatDef.N.leb_$a2,$adef_Coq.Arith.PeanoNat.Nat.Even_$a1,$adef_Coq.PArith.BinPosDef.Pos.sub_mask_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEI_$a1,$adef_Coq.ZArith.BinIntDef.Z.gtb_$a2,$adef_Coq.NArith.BinNatDef.N.testbit_nat_$a1,$adef_Coq.NArith.BinNatDef.N.lor_$a2,$adef_Coq.Init.Nat.testbit_$a1,$adef_$_case_Coq.Init.Datatypes.bool$164239_$a10,$adef_Coq.NArith.BinNatDef.N.pos_div_eucl_$a2,$adef_Coq.Strings.Ascii.eqb_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3,$adef_Coq.Lists.SetoidList.eqlistA_$a4,$adef_Coq.Init.Specif.exist2_$a4,$adef_Coq.Init.Datatypes.xorb_$a2,$adef_$_prop_96613_$a2,$adef_Coq.Strings.String.String_$a2,$adef_Coq.NArith.BinNatDef.N.modulo_$a2,$adef_Coq.Init.Datatypes.CompEqT_$a3,$adef_Coq.Classes.Morphisms.respectful_$a4,$adef_Coq.micromega.Refl.make_impl_$a4,$adef_Coq.micromega.Tauto.FF_$a4,$adef_Coq.ZArith.BinIntDef.Z.abs_$a1,$adef_Coq.PArith.BinPosDef.Pos.min_$a2,$adef_Coq.NArith.BinNatDef.N.odd_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.In_$a2,$adef_Coq.Init.Nat.leb_$a2,$adef_Coq.NArith.BinNatDef.N.succ_$a1,$adef_Coq.Init.Nat.land_$a2,$adef_Coq.Vectors.Fin.FS_$a2,$adef_Coq.micromega.EnvRing.PExpr_$a1,$adef_Coq.Setoids.Setoid.Setoid_Theory_$a2,$adef_Coq.Init.Peano.ge_$a2,$adef_Coq.Relations.Relation_Operators.clos_refl_trans_1n_$a4,$adef_Coq.FSets.FSetPositive.PositiveSet.is_empty_$a1,$adef_Coq.Lists.SetoidList.NoDupA_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.Subset_$a2,$adef_Coq.PArith.BinPosDef.Pos.leb_$a2,$adef_Coq.Classes.RelationClasses.Reflexive_$a2,$adef_$_prop_164536_$a2,$adef_Coq.Arith.EqNat.eq_nat_$a2,$adef_Coq.Init.Datatypes.nat_rect_$a4,$adef_Coq.micromega.Tauto.A_$a6,$adef_Coq.micromega.Tauto.X_$a5,$adef_Coq.Sorting.Sorted.Sorted_$a3,$adef_Coq.ZArith.BinIntDef.Z.rem_$a2,$adef_$_lam_124630_$a4,$adef_Coq.micromega.RMicromega.CInv_$a1,$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.Nat.pred_$a1,$adef_Coq.PArith.BinPosDef.Pos.ltb_$a2,$adef_Coq.Init.Specif.exist_$a3,$adef_Coq.Arith.PeanoNat.Nat.Odd_$a1,$adef_Coq.ZArith.BinInt.Z.le_$a2,$adef_Coq.Init.Specif.projT1_$a3,$adef_Coq.Reals.Rpow_def.pow_$a2,$adef_Coq.Lists.List.map_$a4,$adef_Coq.PArith.BinPosDef.Pos.compare_cont_$a1,$adef_Coq.micromega.EnvRing.Pinj_$a3,$adef_$_lam_124630_$a2,$adef_Coq.ZArith.BinIntDef.Z.quot_$a2,$adef_Coq.NArith.BinNatDef.N.log2_$a1,$adef_Coq.Init.Nat.shiftr_$a1,$adef_Coq.Init.Datatypes.cons_$a3,$adef_$_prop_111500_$a2,$adef_$_lam_124646_$a2,$adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1,$adef_Coq.Init.Datatypes.pair_$a4,$adef_Coq.ZArith.BinIntDef.Z.shiftl_$a2,$adef_Coq.PArith.BinPosDef.Pos.IsPos_$a1,$adef_Coq.Init.Nat.sqrt_iter_$a4,$adef_Coq.FSets.FSetPositive.PositiveSet.union_$a2,$adef_Coq.Init.Nat.bitwise_$a4,$adef_Coq.PArith.BinPosDef.Pos.max_$a2,$adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a2,$adef_Coq.Init.Datatypes.Some_$a2,$adef_Coq.micromega.EnvRing.Pc_$a2,$adef_Coq.Numbers.BinNums.Zpos_$a1,$adef_Coq.NArith.BinNatDef.N.double_$a1,$adef_Coq.Init.Datatypes.list_$a1,$adef_Coq.ZArith.BinInt.Z.lnot_$a1,$adef_Coq.Init.Nat.sub_$a2,$adef_Coq.PArith.BinPos.Pos.SubMaskSpec_$a3,$adef_Coq.micromega.Tauto.clause_$a2,$adef_Coq.NArith.BinNatDef.N.add_$a2,$adef_$_prop_166141_$a2,$adef_Coq.ZArith.BinInt.Z.divide_$a2,$adef_Coq.PArith.BinPosDef.Pos.gcd_$a2,$adef_Coq.Bool.Bool.ReflectF_$a1,$adef_Coq.micromega.EnvRing.PEX_$a2,$adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a11,$adef_Coq.Bool.Bool.ReflectT_$a1,$adef_$_case_Coq.Init.Datatypes.bool$164264_$a8,$adef_Coq.Lists.List.Forall_$a3,$adef_Coq.QArith.QArith_base.Qplus_$a2,$adef_Coq.NArith.BinNatDef.N.lxor_$a2,$adef_Coq.NArith.BinNatDef.N.compare_$a2,$adef_Coq.PArith.BinPosDef.Pos.lxor_$a2,$adef_Coq.Init.Datatypes.fst_$a3,$adef_Coq.Reals.Rbasic_fun.Rabs_$a1,$adef_Coq.ZArith.Zpower.shift_nat_$a2,$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.micromega.Tauto.N_$a5,$adef_Coq.Lists.SetoidList.equivlistA_$a4,$adef_Coq.Init.Nat.min_$a2,$adef_Coq.Init.Specif.existT2_$a6,$adef_Coq.ZArith.BinInt.Zne_$a2,$adef_Coq.PArith.BinPosDef.Pos.compare_$a2,$adef_Coq.micromega.ZMicromega.Vars.Facts.MP.Add_$a3,$adef_Coq.ZArith.BinIntDef.Z.div_$a2,$adef_Coq.PArith.BinPosDef.Pos.pow_$a2,$adef_Coq.Bool.Bool.Is_true_$a1,$adef_Coq.Lists.List.fold_right_$a5,$adef_Coq.FSets.FSetPositive.PositiveSet.For_all_$a2,$adef_Coq.Init.Nat.odd_$a1,$adef_Coq.Lists.List.tl_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.equal_$a2,$adef_Coq.NArith.BinNatDef.N.even_$a1,$adef_$_fix_78273_1_add_carry_$a2,$adef_Coq.Bool.Bool.leb_$a2,$adef_$_prop_96612_$a2,$adef_Coq.Lists.List.NoDup_$a2,$adef_Coq.Vectors.VectorDef.nil_$a1,$adef_Coq.NArith.BinNat.N.le_alt_$a2,$adef_Coq.Init.Specif.left_$a2,$adef_Coq.Lists.SetoidList.compat_bool_$a3,$adef_$_lam_124638_$a2,$adef_Coq.NArith.BinNatDef.N.ltb_$a2,$adef_Coq.Init.Specif.sigT_$a2,$adef_$_lam_124646_$a4,$adef_Coq.micromega.RingMicromega.NFormula_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.fold_$a4,$adef_Coq.ZArith.BinIntDef.Z.pow_$a2,$adef_Coq.Relations.Relation_Operators.clos_refl_trans_n1_$a4,$adef_$_case_Coq.Init.Datatypes.bool$78562_$a4,$adef_Coq.micromega.EnvRing.PX_$a4,$adef_Coq.micromega.EnvRing.PEadd_$a3,$adef_Coq.PArith.BinPosDef.Pos.shiftl_$a2,$adef_Coq.Init.Specif.sig2_$a3,$adef_Coq.Init.Datatypes.length_$a2,$adef_Coq.NArith.BinNatDef.N.eqb_$a2,$adef_Coq.NArith.BinNat.N.eqf_$a2,$adef_$_prop_126724_$a2,$adef_Coq.NArith.BinNat.N.le_$a2,$adef_Coq.Classes.RelationClasses.PreOrder_$a2,$adef_Coq.Init.Nat.divmod_$a4,$adef_Coq.PArith.BinPosDef.Pos.of_succ_nat_$a1,$adef_Coq.micromega.EnvRing.PEsub_$a3,$adef_Coq.PArith.BinPosDef.Pos.add_$a2,$adef_Coq.Init.Nat.double_$a1,$adef_Coq.QArith.QArith_base.Qopp_$a1,$adef_Coq.Init.Peano.gt_$a2,$tdef_$_type_183,$tdef_$_type_76334,$tdef_$_type_755,$tdef_$_type_211,$tdef_$_type_87987,$tdef_$_type_76209,$tdef_$_type_721,$tdef_$_type_2044,$tdef_$_type_116586,$tdef_$_type_107608,$tdef_$_type_2048,$tdef_$_type_168915,$tdef_$_type_79094,$tdef_$_type_96610,$tdef_$_type_1992,$tdef_$_type_127967,$tdef_$_type_110952,$tdef_$_type_98065,$tdef_$_type_75718,$tdef_$_type_116581,$tdef_$_type_108288,$tdef_Coq.Init.Specif.sigT2,$tdef_$_type_75159,$tdef_$_type_108014,$tdef_$_type_76351,$tdef_$_type_81652,$tdef_$_type_81570,$tdef_$_type_105322,$tdef_$_type_95372,$tdef_$_type_78608,$tdef_$_type_78181,$tdef_$_type_110900,$tdef_$_type_104,$tdef_$_type_96943,$tdef_Coq.Init.Datatypes.bool,$tdef_$_type_104284,$tdef_Coq.Init.Datatypes.list,$tdef_$_type_78000,$tdef_$_type_79099,$tdef_$_type_78579,$tdef_Coq.Structures.OrdersTac.ord,$tdef_$_type_107643,$tdef_Coq.micromega.EnvRing.PExpr,$tdef_Coq.Init.Datatypes.option,$tdef_$_type_1495,$tdef_$_type_121863,$tdef_$_type_1024,$tdef_$_type_2023,$tdef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$tdef_$_type_104976,$tdef_$_type_116610,$tdef_$_type_90371,$tdef_$_type_80840,$tdef_$_type_1724,$tdef_$_type_98155,$tdef_$_type_108403,$tdef_$_type_96946,$tdef_$_type_102577,$tdef_Coq.FSets.FSetPositive.PositiveSet.elt,$tdef_$_type_126791,$tdef_$_type_96649,$tdef_$_type_105991,$tdef_$_type_100246,$tdef_$_type_2013,$tdef_$_type_649,$tdef_Coq.setoid_ring.Ring_polynom.Mon,$tdef_Coq.Init.Datatypes.comparison,$tdef_$_type_124778,$tdef_$_type_100293,$tdef_$_type_113855,$tdef_$_type_260,$tdef_$_type_92293,$tdef_Coq.micromega.Tauto.GFormula,$tdef_Coq.Numbers.BinNums.N,$tdef_Coq.Init.Specif.sig2,$tdef_$_type_80825,$tdef_$_type_78598,$tdef_Coq.Init.Specif.sumbool,$tdef_$_type_79080,$tdef_$_type_90422,$tdef_$_type_168979,$tdef_$_type_96794,$tdef_$_type_81622,$tdef_$_type_111508,$tdef_$_type_97863,$tdef_Coq.Reals.Rdefinitions.R,$tdef_$_type_80999,$tdef_$_type_103592,$tdef_$_type_96681,$tdef_$_type_101,$tdef_$_type_111409,$tdef_$_type_748,$tdef_$_type_166677,$tdef_$_type_164508,$tdef_$_type_91368,$tdef_$_type_89007,$tdef_$_type_81078,$tdef_$_type_121840,$tdef_$_type_75071,$tdef_$_type_100371,$tdef_$_type_102923,$tdef_Coq.FSets.FSetPositive.PositiveSet.t,$tdef_$_type_92410,$tdef_Coq.micromega.RMicromega.Rcst,$tdef_Coq.Init.Datatypes.unit,$tdef_$_type_80795,$tdef_Coq.micromega.RingMicromega.PolEnv,$tdef_$_type_90679,$tdef_$_type_90347,$tdef_$_type_76314,$tdef_$_type_1732,$tdef_Coq.Init.Specif.sig,$tdef_$_type_75111,$tdef_$_type_168386,$tdef_$_type_1276,$tdef_Coq.Init.Datatypes.sum,$tdef_$_type_96948,$tdef_$_type_75099,$tdef_$_type_113942,$tdef_$_type_206,$tdef_$_type_1675,$tdef_$_type_92356,$tdef_Coq.Strings.Ascii.ascii,$tdef_Coq.FSets.FSetPositive.PositiveSet.tree,$tdef_$_type_77726,$tdef_$_type_110969,$tdef_Coq.Relations.Relation_Definitions.relation,$tdef_$_type_110782,$tdef_$_type_100250,$tdef_$_type_97964,$tdef_$_type_80876,$tdef_$_type_78360,$tdef_$_type_78395,$tdef_$_type_77995,$tdef_$_type_166468,$tdef_$_type_108295,$tdef_Prop,$tdef_$_type_75114,$tdef_$_type_92230,$tdef_Coq.micromega.RingMicromega.Op2,$tdef_$_type_78467,$tdef_$_type_271,$tdef_$_type_1500,$tdef_Coq.Init.Byte.byte,$tdef_$_type_98357,$tdef_$_type_79389,$tdef_$_type_639,$tdef_$_type_95380,$tdef_$_type_1515,$tdef_$_type_79108,$tdef_$_type_80842,$tdef_$_type_168983,$tdef_Coq.Strings.String.string,$tdef_$_type_101048,$tdef_$_type_166602,$tdef_$_type_111512,$tdef_$_type_110934,$tdef_$_type_76310,$tdef_$_type_78420,$tdef_Coq.micromega.RingMicromega.Op1,$tdef_Coq.Init.Datatypes.CompareSpecT,$tdef_Coq.Init.Specif.sigT,$tdef_$_type_110856,$tdef_$_type_168955,$tdef_$_type_100285,$tdef_$_type_2029,$tdef_$_type_168437,$tdef_$_type_105645,$tdef_$_type_75030,$tdef_$_type_78836,$tdef_$_type_76357,$tdef_$_type_103938,$tdef_$_type_95388,$tdef_Coq.micromega.EnvRing.Pol,$tdef_$_type_109012,$tdef_$_type_81783,$tdef_$_type_829,$tdef_$_type_96509,$tdef_$_type_110739,$tdef_$_type_1707,$tdef_$_type_657,$tdef_$_type_2065,$tdef_$_type_108368,$tdef_$_type_765,$tdef_$_type_96677,$tdef_$_type_80803,$tdef_$_type_110917,$tdef_$_type_124683,$tdef_$_type_78604,$tdef_$_type_104630,$tdef_$_type_78568,$tdef_$_type_90441,$tdef_$_type_168935,$tdef_$_type_78595,$tdef_$_type_106337,$tdef_Coq.Bool.Bool.reflect,$tdef_$_type_164534,$tdef_Coq.setoid_ring.Ring_polynom.Pol,$tdef_$_type_6,$tdef_$_type_168973,$tdef_$_type_90855,$tdef_$_type_1999,$tdef_LF.Basics.bool,$tdef_$_type_108321,$tdef_$_type_90427,$tdef_$_type_81808,$tdef_$_type_98458,$tdef_Coq.Numbers.BinNums.Z,$tdef_$_type_77704,$tdef_$_type_312,$tdef_$_type_92473,$tdef_Coq.QArith.QArith_base.Q,$tdef_Coq.Numbers.BinNums.positive,$tdef_Coq.Init.Datatypes.nat,$tdef_$_type_746,$tdef_$_type_113825,$tdef_$_type_111486,$tdef_$_type_107329,$tdef_$_type_75139,$tdef_$_type_103269,$tdef_$_type_80777,$tdef_$_type_75849,$tdef_$_type_1013,$tdef_Coq.Init.Datatypes.prod,$tdef_$_type_110923,$tdef_Coq.micromega.RingMicromega.Formula,$tdef_$_type_78303,$tdef_Coq.micromega.RingMicromega.PolC,$tdef_Coq.setoid_ring.Ring_polynom.PExpr,$tdef_$_type_75127,$tdef_$_type_106660,$tdef_$_type_77991,$tdef_$_type_110821,$tdef_$_type_90675,$tdef_$_type_121813,$tdef_$_type_95422,$tdef_$_type_706,$tdef_$_type_781,$tdef_$_type_90435,$tdef_$_type_75743,$tdef_$_type_801,$tdef_Coq.Vectors.VectorDef.t,$tdef_$_type_81793,$tdef_$_type_98256,$tdef_$_type_13,$tdef_$_type_76317,$tdef_$_type_106983,$tdef_$_type_90432,$tdef_$_type_806,$tdef_$_type_111447,$tdef_Type,$tdef_Coq.PArith.BinPosDef.Pos.mask,$tdef_$_type_113873,$tdef_$_type_285,$tdef_$_type_685,$tdef_$_type_839,$tdef_$_type_8,$tdef_$_type_2207,$tdef_$_type_75034,$tdef_Coq.Vectors.Fin.t,$tdef_$_type_78882,$tdef_$_type_165405,$tdef_$_type_81179,$tdef_$_type_81811,$tdef_$_type_1281,$tdef_$_type_77737,$tdef_$_type_78364,$tdef_$_type_717,$tdef_$_type_168314,$tdef_$_type_100301,$tdef_$_type_1696,$tdef_$_type_168992,$tdef_$_type_75069,$tdef_$_type_2132] % 15.66/15.88 =============================================================== % 15.66/15.88 % 15.66/15.88 Combined formula: 2363 axiom(s) => conjecture % 15.66/15.88 % 15.66/15.88 % Equality/functions detected -> nanoCoP oracle mode % 15.66/15.88 nanoCoP : % 15.66/15.88 % 10,288,238 inferences, 11.674 CPU in 11.673 seconds (100% CPU, 881332 Lips) % 15.66/15.88 % 15.66/15.88 % nanoCoP proof (equality/functions) % 15.66/15.88 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 15.66/15.88 % 15.66/15.88 % SZS output end Proof %------------------------------------------------------------------------------