%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SEV664+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 : n004.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:51 PM UTC 2026 % Result : Theorem 11.02s 11.72s % Output : Proof 11.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV664+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.15/0.33 % Computer : n004.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:04:48 EDT 2026 % 0.15/0.33 % CPUTime : % 11.02/11.72 % SZS status Theorem % 11.02/11.72 % SZS output start Proof % 11.02/11.73 % 11.02/11.73 =============================================================== % 11.02/11.73 TPTP Problem: _HAMMER_GOAL (conjecture with 2538 axiom(s)) % 11.02/11.73 Axioms: [_HAMMER_COQ_TRUE,_HAMMER_COQ_FALSE,_HAMMER_COQ_TYPE_TYPE,$_case_Coq.Init.Datatypes.bool$102739,$_case_Coq.Init.Datatypes.bool$142229,$_case_Coq.Init.Datatypes.comparison$165612,$_case_Coq.Init.Datatypes.nat$21811,$_case_Coq.Init.Datatypes.nat$21833,$_case_Coq.Init.Datatypes.prod$8582,$_case_Coq.Numbers.BinNums.Z$21828,$_def_$_let_var_6_p_21874_21877,$_def_$_let_var_6_p_21876_21878,$_def_Coq.Arith.EqNat.eq_nat,$_def_Coq.Arith.PeanoNat.Nat.b2n,$_def_Coq.Arith.PeanoNat.Nat.divide,$_def_Coq.Arith.PeanoNat.Nat.eqf,$_def_Coq.Bool.Bool.Is_true,$_def_Coq.Bool.Bool.eqb,$_def_Coq.Bool.Zerob.zerob,$_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.elt,$_def_Coq.FSets.FSetPositive.PositiveSet.empty,$_def_Coq.FSets.FSetPositive.PositiveSet.eq,$_def_Coq.FSets.FSetPositive.PositiveSet.equal,$_def_Coq.FSets.FSetPositive.PositiveSet.is_empty,$_def_Coq.FSets.FSetPositive.PositiveSet.mem,$_def_Coq.FSets.FSetPositive.PositiveSet.rev_append,$_def_Coq.FSets.FSetPositive.PositiveSet.t,$_def_Coq.Init.Datatypes.CompOpp,$_def_Coq.Init.Datatypes.CompSpecT,$_def_Coq.Init.Datatypes.IDProp,$_def_Coq.Init.Datatypes.andb,$_def_Coq.Init.Datatypes.app,$_def_Coq.Init.Datatypes.fst,$_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.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.sqrt,$_def_Coq.Init.Nat.sqrt_iter,$_def_Coq.Init.Nat.sub,$_def_Coq.Init.Nat.testbit,$_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.Init.Wf.well_founded,$_def_Coq.Lists.List.In,$_def_Coq.Lists.List.fold_left,$_def_Coq.Lists.List.fold_right,$_def_Coq.Lists.List.last,$_def_Coq.Lists.List.map,$_def_Coq.Lists.List.nth,$_def_Coq.Lists.SetoidList.compat_bool,$_def_Coq.Lists.SetoidList.compat_op,$_def_Coq.Lists.SetoidList.transpose,$_def_Coq.Logic.Decidable.decidable,$_def_Coq.Logic.EqdepFacts.Eq_dep_eq_on,$_def_Coq.Logic.EqdepFacts.Eq_rect_eq,$_def_Coq.Logic.EqdepFacts.Eq_rect_eq_on,$_def_Coq.Logic.EqdepFacts.Streicher_K_on_,$_def_Coq.Logic.EqdepFacts.UIP_,$_def_Coq.Logic.EqdepFacts.UIP_on_,$_def_Coq.Logic.EqdepFacts.UIP_refl_on_,$_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.lt,$_def_Coq.NArith.BinNatDef.N.add,$_def_Coq.NArith.BinNatDef.N.compare,$_def_Coq.NArith.BinNatDef.N.div,$_def_Coq.NArith.BinNatDef.N.div2,$_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.log2,$_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.pow,$_def_Coq.NArith.BinNatDef.N.pred,$_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.to_nat,$_def_Coq.PArith.BinPos.Pos.le,$_def_Coq.PArith.BinPos.Pos.lt,$_def_Coq.PArith.BinPos.Pos.switch_Eq,$_def_Coq.PArith.BinPosDef.Pos.add,$_def_Coq.PArith.BinPosDef.Pos.compare,$_def_Coq.PArith.BinPosDef.Pos.iter,$_def_Coq.PArith.BinPosDef.Pos.iter_op,$_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,$_def_Coq.PArith.BinPosDef.Pos.sub,$_def_Coq.PArith.BinPosDef.Pos.succ,$_def_Coq.PArith.BinPosDef.Pos.to_nat,$_def_Coq.QArith.QArith_base.Qden,$_def_Coq.QArith.QArith_base.Qnum,$_def_Coq.Reals.RIneq.Rsqr,$_def_Coq.Reals.Rdefinitions.IZR,$_def_Coq.Reals.Rdefinitions.Rdiv,$_def_Coq.Reals.Rdefinitions.Rge,$_def_Coq.Reals.Rdefinitions.Rgt,$_def_Coq.Reals.Rdefinitions.Rle,$_def_Coq.Reals.Rdefinitions.Rminus,$_def_Coq.Reals.Rpow_def.pow,$_def_Coq.Relations.Relation_Definitions.relation,$_def_Coq.Setoids.Setoid.Setoid_Theory,$_def_Coq.Structures.OrderedTypeEx.N_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.N_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.N_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.String_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.String_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.String_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.Z_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.Z_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$_def_Coq.Vectors.VectorDef.fold_right,$_def_Coq.ZArith.BinInt.Z.Bezout,$_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.le,$_def_Coq.ZArith.BinInt.Z.lt,$_def_Coq.ZArith.BinInt.Zne,$_def_Coq.ZArith.BinIntDef.Z.abs,$_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.gcd,$_def_Coq.ZArith.BinIntDef.Z.leb,$_def_Coq.ZArith.BinIntDef.Z.log2,$_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.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.rem,$_def_Coq.ZArith.BinIntDef.Z.sgn,$_def_Coq.ZArith.BinIntDef.Z.sqrt,$_def_Coq.ZArith.BinIntDef.Z.sub,$_def_Coq.ZArith.BinIntDef.Z.succ,$_def_Coq.ZArith.BinIntDef.Z.to_pos,$_def_Coq.ZArith.Zbool.Zeq_bool,$_def_Coq.ZArith.Zdiv.Remainder,$_def_Coq.micromega.Env.Env,$_def_Coq.micromega.Env.jump,$_def_Coq.micromega.Env.nth,$_def_Coq.micromega.Refl.make_conj,$_def_Coq.micromega.Refl.make_impl,$_def_Coq.micromega.RingMicromega.PolEnv,$_def_Coq.micromega.RingMicromega.eval_op2,$_def_Coq.micromega.ZMicromega.Vars.Facts.Add,$_def_Coq.setoid_ring.Field_theory.Fapp,$_def_Coq.setoid_ring.Field_theory.condition,$_def_Coq.setoid_ring.Field_theory.denum,$_def_Coq.setoid_ring.Field_theory.num,$_def_Coq.setoid_ring.Field_theory.rsplit_left,$_def_Coq.setoid_ring.Field_theory.rsplit_right,$_def_Coq.setoid_ring.InitialRing.Nopp,$_def_Coq.setoid_ring.InitialRing.Nsub,$_def_Coq.setoid_ring.InitialRing.gen_phiN,$_def_Coq.setoid_ring.InitialRing.gen_phiZ,$_def_Coq.setoid_ring.InitialRing.triv_div,$_def_Coq.setoid_ring.Ring.bool_eq,$_def_Coq.setoid_ring.Ring_polynom.PEeval,$_def_Coq.setoid_ring.Ring_polynom.Peq,$_def_Coq.setoid_ring.Ring_tac.ring_subst_niter,$_def_Coq.setoid_ring.Ring_theory.IDphi,$_def_Coq.setoid_ring.Ring_theory.SRopp,$_def_Coq.setoid_ring.Ring_theory.SRsub,$_def_Coq.setoid_ring.Ring_theory.get_sign_None,$_def_Coq.setoid_ring.Ring_theory.id_phi_N,$_def_Coq.setoid_ring.Ring_theory.pow_N,$_def_Coq.setoid_ring.Ring_theory.pow_pos,$_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.inl$Coq.Init.Datatypes.inr,$_discrim_Coq.Init.Datatypes.nil$Coq.Init.Datatypes.cons,$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false,$_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright,$_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.Strings.String.EmptyString$Coq.Strings.String.String,$_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ,$_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.EnvRing.mon0$Coq.micromega.EnvRing.zmon,$_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.Field_theory.FEO$Coq.setoid_ring.Field_theory.FEI,$_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_Coq.setoid_ring.Ring_theory.Abstract$Coq.setoid_ring.Ring_theory.Computational,$_fix_20500_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.inl,$_inj_Coq.Init.Datatypes.inr,$_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.inleft,$_inj_Coq.Init.Specif.inright,$_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.RIneq.mknonzeroreal,$_inj_Coq.Reals.Rfunctions.ZintNeg,$_inj_Coq.Reals.Rfunctions.ZintNull,$_inj_Coq.Reals.Rfunctions.ZintPos,$_inj_Coq.Strings.Ascii.Ascii,$_inj_Coq.Strings.String.String,$_inj_Coq.Structures.OrderedType.EQ,$_inj_Coq.Structures.OrderedType.GT,$_inj_Coq.Structures.OrderedType.LT,$_inj_Coq.Vectors.Fin.F1,$_inj_Coq.Vectors.Fin.FS,$_inj_Coq.Vectors.VectorDef.cons,$_inj_Coq.Vectors.VectorDef.nil,$_inj_Coq.ZArith.Znumtheory.Euclid_intro,$_inj_Coq.ZArith.Zpower.Zdiv_rest_proof,$_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.EnvRing.vmon,$_inj_Coq.micromega.EnvRing.zmon,$_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.Field_theory.FEI,$_inj_Coq.setoid_ring.Field_theory.FEO,$_inj_Coq.setoid_ring.Field_theory.FEX,$_inj_Coq.setoid_ring.Field_theory.FEadd,$_inj_Coq.setoid_ring.Field_theory.FEc,$_inj_Coq.setoid_ring.Field_theory.FEdiv,$_inj_Coq.setoid_ring.Field_theory.FEinv,$_inj_Coq.setoid_ring.Field_theory.FEmul,$_inj_Coq.setoid_ring.Field_theory.FEopp,$_inj_Coq.setoid_ring.Field_theory.FEpow,$_inj_Coq.setoid_ring.Field_theory.FEsub,$_inj_Coq.setoid_ring.Field_theory.mk_linear,$_inj_Coq.setoid_ring.Field_theory.mk_rsplit,$_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,$_inj_Coq.setoid_ring.Ring_theory.Computational,$_inj_Coq.setoid_ring.Ring_theory.Morphism,$_inversion_Coq.Arith.Between.between,$_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.BoolSpec,$_inversion_Coq.Init.Datatypes.CompareSpec,$_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.sum,$_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.Init.Specif.sumor,$_inversion_Coq.Init.Wf.Acc,$_inversion_Coq.Lists.List.Forall,$_inversion_Coq.Lists.List.NoDup,$_inversion_Coq.Lists.SetoidList.InA,$_inversion_Coq.Lists.SetoidList.NoDupA,$_inversion_Coq.Logic.EqdepFacts.eq_dep,$_inversion_Coq.Logic.EqdepFacts.eq_dep1,$_inversion_Coq.Numbers.BinNums.N,$_inversion_Coq.Numbers.BinNums.Z,$_inversion_Coq.Numbers.BinNums.positive,$_inversion_Coq.PArith.BinPos.Pos.SqrtSpec,$_inversion_Coq.PArith.BinPos.Pos.SubMaskSpec,$_inversion_Coq.PArith.BinPosDef.Pos.mask,$_inversion_Coq.QArith.QArith_base.Q,$_inversion_Coq.Reals.RIneq.nonzeroreal,$_inversion_Coq.Reals.Rfunctions.Z_spec,$_inversion_Coq.Sorting.Sorted.StronglySorted,$_inversion_Coq.Strings.Ascii.ascii,$_inversion_Coq.Strings.String.string,$_inversion_Coq.Structures.OrderedType.Compare,$_inversion_Coq.Structures.OrderedTypeEx.String_as_OT.lts,$_inversion_Coq.Structures.OrdersTac.ord,$_inversion_Coq.Vectors.Fin.t,$_inversion_Coq.Vectors.VectorDef.t,$_inversion_Coq.ZArith.Znumtheory.Bezout,$_inversion_Coq.ZArith.Znumtheory.Euclid,$_inversion_Coq.ZArith.Znumtheory.Zis_gcd,$_inversion_Coq.ZArith.Zpower.Zdiv_rest_proofs,$_inversion_Coq.micromega.EnvRing.Mon,$_inversion_Coq.micromega.EnvRing.PExpr,$_inversion_Coq.micromega.EnvRing.Pol,$_inversion_Coq.micromega.OrderedRing.SOR,$_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.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_elt_Prop,$_inversion_Coq.micromega.ZMicromega.is_diff_env_elt,$_inversion_Coq.setoid_ring.Field_theory.FExpr,$_inversion_Coq.setoid_ring.Field_theory.almost_field_theory,$_inversion_Coq.setoid_ring.Field_theory.linear,$_inversion_Coq.setoid_ring.Field_theory.rsplit,$_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.almost_ring_theory,$_inversion_Coq.setoid_ring.Ring_theory.div_theory,$_inversion_Coq.setoid_ring.Ring_theory.power_theory,$_inversion_Coq.setoid_ring.Ring_theory.ring_eq_ext,$_inversion_Coq.setoid_ring.Ring_theory.ring_kind,$_inversion_Coq.setoid_ring.Ring_theory.ring_morph,$_inversion_Coq.setoid_ring.Ring_theory.semi_morph,$_inversion_Coq.setoid_ring.Ring_theory.sign_theory,$_inversion_Coq.setoid_ring.Ring_theory.sring_eq_ext,$_lam_103102,$_lam_12266,$_lam_14771,$_lam_14779,$_lam_14787,$_lam_14795,$_prop_10581,$_prop_10582,$_prop_166330,$_prop_20885,$_prop_23380,$_prop_23381,$_prop_23382,$_prop_23383,$_prop_23384,$_prop_23385,$_prop_23386,$_prop_32246,$_prop_440,$_prop_441,$_type_10047,$_type_10051,$_type_10055,$_type_10101,$_type_10113,$_type_10125,$_type_10127,$_type_10132,$_type_101786,$_type_10187,$_type_10200,$_type_10202,$_type_1022,$_type_10221,$_type_102742,$_type_102836,$_type_103177,$_type_103179,$_type_10574,$_type_10579,$_type_10585,$_type_1104,$_type_11789,$_type_11847,$_type_11910,$_type_1197,$_type_12041,$_type_12066,$_type_12105,$_type_12109,$_type_12123,$_type_12222,$_type_12237,$_type_12251,$_type_12719,$_type_1279,$_type_12820,$_type_12921,$_type_13011,$_type_13112,$_type_13213,$_type_13314,$_type_13480,$_type_13499,$_type_13519,$_type_13622,$_type_13632,$_type_13638,$_type_13651,$_type_13656,$_type_13667,$_type_1372,$_type_1381,$_type_13833,$_type_13882,$_type_1390,$_type_141300,$_type_145287,$_type_145293,$_type_14832,$_type_15251,$_type_15259,$_type_15262,$_type_15391,$_type_154381,$_type_154397,$_type_154763,$_type_155143,$_type_156168,$_type_156173,$_type_158368,$_type_158399,$_type_159221,$_type_159569,$_type_16,$_type_16600,$_type_16603,$_type_16606,$_type_166265,$_type_166277,$_type_166286,$_type_166294,$_type_166299,$_type_166308,$_type_166313,$_type_166325,$_type_166378,$_type_166386,$_type_166389,$_type_16640,$_type_166723,$_type_16731,$_type_16754,$_type_16777,$_type_16800,$_type_16818,$_type_16844,$_type_16862,$_type_17120,$_type_17245,$_type_17370,$_type_17495,$_type_17620,$_type_17745,$_type_17856,$_type_17892,$_type_17903,$_type_17934,$_type_17946,$_type_17988,$_type_18023,$_type_18034,$_type_18054,$_type_18058,$_type_18076,$_type_18093,$_type_18097,$_type_18100,$_type_18117,$_type_183,$_type_18407,$_type_20068,$_type_20144,$_type_20153,$_type_20164,$_type_20269,$_type_20462,$_type_20466,$_type_20530,$_type_20574,$_type_20742,$_type_2076,$_type_2081,$_type_20841,$_type_2090,$_type_20994,$_type_21039,$_type_2115,$_type_2135,$_type_22,$_type_22657,$_type_22667,$_type_22693,$_type_22701,$_type_22709,$_type_22749,$_type_22757,$_type_22765,$_type_22791,$_type_22874,$_type_23298,$_type_23408,$_type_23504,$_type_23614,$_type_23691,$_type_23696,$_type_23727,$_type_24,$_type_2404,$_type_24262,$_type_24608,$_type_2469,$_type_2493,$_type_24954,$_type_2507,$_type_2514,$_type_25277,$_type_25623,$_type_25969,$_type_26315,$_type_26661,$_type_27007,$_type_27330,$_type_27676,$_type_28022,$_type_28345,$_type_28668,$_type_29014,$_type_2931,$_type_29362,$_type_29371,$_type_29419,$_type_29456,$_type_29472,$_type_29568,$_type_29571,$_type_29693,$_type_29696,$_type_29701,$_type_29709,$_type_29712,$_type_29725,$_type_29734,$_type_29739,$_type_29742,$_type_29747,$_type_29750,$_type_29833,$_type_29857,$_type_29886,$_type_29893,$_type_29957,$_type_30063,$_type_30078,$_type_301,$_type_30661,$_type_30688,$_type_307,$_type_30714,$_type_31241,$_type_31363,$_type_31374,$_type_31633,$_type_31798,$_type_31818,$_type_31840,$_type_31858,$_type_31864,$_type_31881,$_type_31887,$_type_31893,$_type_31898,$_type_31901,$_type_31952,$_type_322,$_type_32239,$_type_32250,$_type_3227,$_type_32317,$_type_32357,$_type_32412,$_type_32438,$_type_32443,$_type_32451,$_type_32468,$_type_32472,$_type_3420,$_type_355,$_type_364,$_type_367,$_type_373,$_type_386,$_type_393,$_type_397,$_type_4,$_type_400,$_type_405,$_type_417,$_type_438,$_type_4596,$_type_462,$_type_470,$_type_4850,$_type_4913,$_type_493,$_type_4976,$_type_5030,$_type_5093,$_type_5300,$_type_5330,$_type_5354,$_type_5384,$_type_5414,$_type_5438,$_type_547,$_type_5471,$_type_5495,$_type_550,$_type_5522,$_type_5921,$_type_594,$_type_6134,$_type_6347,$_type_640,$_type_6542,$_type_6755,$_type_6968,$_type_7181,$_type_7394,$_type_7589,$_type_7802,$_type_7997,$_type_8139,$_type_8158,$_type_8172,$_type_8327,$_type_836,$_type_8377,$_type_8427,$_type_8469,$_type_8519,$_type_8595,$_type_8704,$_type_8748,$_type_8784,$_type_8828,$_type_8840,$_type_8847,$_type_8904,$_type_8909,$_type_8915,$_type_8935,$_type_8976,$_type_9034,$_type_9046,$_type_9212,$_type_9218,$_type_9228,$_type_929,$_type_99424,$_type_99548,$_typeof_Coq.Arith.EqNat.eq_nat,$_typeof_Coq.Arith.PeanoNat.Nat.b2n,$_typeof_Coq.Arith.PeanoNat.Nat.divide,$_typeof_Coq.Arith.PeanoNat.Nat.eqf,$_typeof_Coq.Bool.Bool.Is_true,$_typeof_Coq.Bool.Bool.eqb,$_typeof_Coq.Bool.Bool.reflect,$_typeof_Coq.Bool.Zerob.zerob,$_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.elt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.eq,$_typeof_Coq.FSets.FSetPositive.PositiveSet.equal,$_typeof_Coq.FSets.FSetPositive.PositiveSet.is_empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.mem,$_typeof_Coq.FSets.FSetPositive.PositiveSet.rev_append,$_typeof_Coq.FSets.FSetPositive.PositiveSet.t,$_typeof_Coq.FSets.FSetPositive.PositiveSet.tree,$_typeof_Coq.Init.Byte.byte,$_typeof_Coq.Init.Byte.x00,$_typeof_Coq.Init.Byte.x01,$_typeof_Coq.Init.Byte.x02,$_typeof_Coq.Init.Byte.x03,$_typeof_Coq.Init.Byte.x04,$_typeof_Coq.Init.Byte.x05,$_typeof_Coq.Init.Byte.x06,$_typeof_Coq.Init.Byte.x07,$_typeof_Coq.Init.Byte.x08,$_typeof_Coq.Init.Byte.x09,$_typeof_Coq.Init.Byte.x0a,$_typeof_Coq.Init.Byte.x0b,$_typeof_Coq.Init.Byte.x0c,$_typeof_Coq.Init.Byte.x0d,$_typeof_Coq.Init.Byte.x0e,$_typeof_Coq.Init.Byte.x0f,$_typeof_Coq.Init.Byte.x10,$_typeof_Coq.Init.Byte.x11,$_typeof_Coq.Init.Byte.x12,$_typeof_Coq.Init.Byte.x13,$_typeof_Coq.Init.Byte.x14,$_typeof_Coq.Init.Byte.x15,$_typeof_Coq.Init.Byte.x16,$_typeof_Coq.Init.Byte.x17,$_typeof_Coq.Init.Byte.x18,$_typeof_Coq.Init.Byte.x19,$_typeof_Coq.Init.Byte.x1a,$_typeof_Coq.Init.Byte.x1b,$_typeof_Coq.Init.Byte.x1c,$_typeof_Coq.Init.Byte.x1d,$_typeof_Coq.Init.Byte.x1e,$_typeof_Coq.Init.Byte.x1f,$_typeof_Coq.Init.Byte.x20,$_typeof_Coq.Init.Byte.x21,$_typeof_Coq.Init.Byte.x22,$_typeof_Coq.Init.Byte.x23,$_typeof_Coq.Init.Byte.x24,$_typeof_Coq.Init.Byte.x25,$_typeof_Coq.Init.Byte.x26,$_typeof_Coq.Init.Byte.x27,$_typeof_Coq.Init.Byte.x28,$_typeof_Coq.Init.Byte.x29,$_typeof_Coq.Init.Byte.x2a,$_typeof_Coq.Init.Byte.x2b,$_typeof_Coq.Init.Byte.x2c,$_typeof_Coq.Init.Byte.x2d,$_typeof_Coq.Init.Byte.x2e,$_typeof_Coq.Init.Byte.x2f,$_typeof_Coq.Init.Byte.x30,$_typeof_Coq.Init.Byte.x31,$_typeof_Coq.Init.Byte.x32,$_typeof_Coq.Init.Byte.x33,$_typeof_Coq.Init.Byte.x34,$_typeof_Coq.Init.Byte.x35,$_typeof_Coq.Init.Byte.x36,$_typeof_Coq.Init.Byte.x37,$_typeof_Coq.Init.Byte.x38,$_typeof_Coq.Init.Byte.x39,$_typeof_Coq.Init.Byte.x3a,$_typeof_Coq.Init.Byte.x3b,$_typeof_Coq.Init.Byte.x3c,$_typeof_Coq.Init.Byte.x3d,$_typeof_Coq.Init.Byte.x3e,$_typeof_Coq.Init.Byte.x3f,$_typeof_Coq.Init.Byte.x40,$_typeof_Coq.Init.Byte.x41,$_typeof_Coq.Init.Byte.x42,$_typeof_Coq.Init.Byte.x43,$_typeof_Coq.Init.Byte.x44,$_typeof_Coq.Init.Byte.x45,$_typeof_Coq.Init.Byte.x46,$_typeof_Coq.Init.Byte.x47,$_typeof_Coq.Init.Byte.x48,$_typeof_Coq.Init.Byte.x49,$_typeof_Coq.Init.Byte.x4a,$_typeof_Coq.Init.Byte.x4b,$_typeof_Coq.Init.Byte.x4c,$_typeof_Coq.Init.Byte.x4d,$_typeof_Coq.Init.Byte.x4e,$_typeof_Coq.Init.Byte.x4f,$_typeof_Coq.Init.Byte.x50,$_typeof_Coq.Init.Byte.x51,$_typeof_Coq.Init.Byte.x52,$_typeof_Coq.Init.Byte.x53,$_typeof_Coq.Init.Byte.x54,$_typeof_Coq.Init.Byte.x55,$_typeof_Coq.Init.Byte.x56,$_typeof_Coq.Init.Byte.x57,$_typeof_Coq.Init.Byte.x58,$_typeof_Coq.Init.Byte.x59,$_typeof_Coq.Init.Byte.x5a,$_typeof_Coq.Init.Byte.x5b,$_typeof_Coq.Init.Byte.x5c,$_typeof_Coq.Init.Byte.x5d,$_typeof_Coq.Init.Byte.x5e,$_typeof_Coq.Init.Byte.x5f,$_typeof_Coq.Init.Byte.x60,$_typeof_Coq.Init.Byte.x61,$_typeof_Coq.Init.Byte.x62,$_typeof_Coq.Init.Byte.x63,$_typeof_Coq.Init.Byte.x64,$_typeof_Coq.Init.Byte.x65,$_typeof_Coq.Init.Byte.x66,$_typeof_Coq.Init.Byte.x67,$_typeof_Coq.Init.Byte.x68,$_typeof_Coq.Init.Byte.x69,$_typeof_Coq.Init.Byte.x6a,$_typeof_Coq.Init.Byte.x6b,$_typeof_Coq.Init.Byte.x6c,$_typeof_Coq.Init.Byte.x6d,$_typeof_Coq.Init.Byte.x6e,$_typeof_Coq.Init.Byte.x6f,$_typeof_Coq.Init.Byte.x70,$_typeof_Coq.Init.Byte.x71,$_typeof_Coq.Init.Byte.x72,$_typeof_Coq.Init.Byte.x73,$_typeof_Coq.Init.Byte.x74,$_typeof_Coq.Init.Byte.x75,$_typeof_Coq.Init.Byte.x76,$_typeof_Coq.Init.Byte.x77,$_typeof_Coq.Init.Byte.x78,$_typeof_Coq.Init.Byte.x79,$_typeof_Coq.Init.Byte.x7a,$_typeof_Coq.Init.Byte.x7b,$_typeof_Coq.Init.Byte.x7c,$_typeof_Coq.Init.Byte.x7d,$_typeof_Coq.Init.Byte.x7e,$_typeof_Coq.Init.Byte.x7f,$_typeof_Coq.Init.Byte.x80,$_typeof_Coq.Init.Byte.x81,$_typeof_Coq.Init.Byte.x82,$_typeof_Coq.Init.Byte.x83,$_typeof_Coq.Init.Byte.x84,$_typeof_Coq.Init.Byte.x85,$_typeof_Coq.Init.Byte.x86,$_typeof_Coq.Init.Byte.x87,$_typeof_Coq.Init.Byte.x88,$_typeof_Coq.Init.Byte.x89,$_typeof_Coq.Init.Byte.x8a,$_typeof_Coq.Init.Byte.x8b,$_typeof_Coq.Init.Byte.x8c,$_typeof_Coq.Init.Byte.x8d,$_typeof_Coq.Init.Byte.x8e,$_typeof_Coq.Init.Byte.x8f,$_typeof_Coq.Init.Byte.x90,$_typeof_Coq.Init.Byte.x91,$_typeof_Coq.Init.Byte.x92,$_typeof_Coq.Init.Byte.x93,$_typeof_Coq.Init.Byte.x94,$_typeof_Coq.Init.Byte.x95,$_typeof_Coq.Init.Byte.x96,$_typeof_Coq.Init.Byte.x97,$_typeof_Coq.Init.Byte.x98,$_typeof_Coq.Init.Byte.x99,$_typeof_Coq.Init.Byte.x9a,$_typeof_Coq.Init.Byte.x9b,$_typeof_Coq.Init.Byte.x9c,$_typeof_Coq.Init.Byte.x9d,$_typeof_Coq.Init.Byte.x9e,$_typeof_Coq.Init.Byte.x9f,$_typeof_Coq.Init.Byte.xa0,$_typeof_Coq.Init.Byte.xa1,$_typeof_Coq.Init.Byte.xa2,$_typeof_Coq.Init.Byte.xa3,$_typeof_Coq.Init.Byte.xa4,$_typeof_Coq.Init.Byte.xa5,$_typeof_Coq.Init.Byte.xa6,$_typeof_Coq.Init.Byte.xa7,$_typeof_Coq.Init.Byte.xa8,$_typeof_Coq.Init.Byte.xa9,$_typeof_Coq.Init.Byte.xaa,$_typeof_Coq.Init.Byte.xab,$_typeof_Coq.Init.Byte.xac,$_typeof_Coq.Init.Byte.xad,$_typeof_Coq.Init.Byte.xae,$_typeof_Coq.Init.Byte.xaf,$_typeof_Coq.Init.Byte.xb0,$_typeof_Coq.Init.Byte.xb1,$_typeof_Coq.Init.Byte.xb2,$_typeof_Coq.Init.Byte.xb3,$_typeof_Coq.Init.Byte.xb4,$_typeof_Coq.Init.Byte.xb5,$_typeof_Coq.Init.Byte.xb6,$_typeof_Coq.Init.Byte.xb7,$_typeof_Coq.Init.Byte.xb8,$_typeof_Coq.Init.Byte.xb9,$_typeof_Coq.Init.Byte.xba,$_typeof_Coq.Init.Byte.xbb,$_typeof_Coq.Init.Byte.xbc,$_typeof_Coq.Init.Byte.xbd,$_typeof_Coq.Init.Byte.xbe,$_typeof_Coq.Init.Byte.xbf,$_typeof_Coq.Init.Byte.xc0,$_typeof_Coq.Init.Byte.xc1,$_typeof_Coq.Init.Byte.xc2,$_typeof_Coq.Init.Byte.xc3,$_typeof_Coq.Init.Byte.xc4,$_typeof_Coq.Init.Byte.xc5,$_typeof_Coq.Init.Byte.xc6,$_typeof_Coq.Init.Byte.xc7,$_typeof_Coq.Init.Byte.xc8,$_typeof_Coq.Init.Byte.xc9,$_typeof_Coq.Init.Byte.xca,$_typeof_Coq.Init.Byte.xcb,$_typeof_Coq.Init.Byte.xcc,$_typeof_Coq.Init.Byte.xcd,$_typeof_Coq.Init.Byte.xce,$_typeof_Coq.Init.Byte.xcf,$_typeof_Coq.Init.Byte.xd0,$_typeof_Coq.Init.Byte.xd1,$_typeof_Coq.Init.Byte.xd2,$_typeof_Coq.Init.Byte.xd3,$_typeof_Coq.Init.Byte.xd4,$_typeof_Coq.Init.Byte.xd5,$_typeof_Coq.Init.Byte.xd6,$_typeof_Coq.Init.Byte.xd7,$_typeof_Coq.Init.Byte.xd8,$_typeof_Coq.Init.Byte.xd9,$_typeof_Coq.Init.Byte.xda,$_typeof_Coq.Init.Byte.xdb,$_typeof_Coq.Init.Byte.xdc,$_typeof_Coq.Init.Byte.xdd,$_typeof_Coq.Init.Byte.xde,$_typeof_Coq.Init.Byte.xdf,$_typeof_Coq.Init.Byte.xe0,$_typeof_Coq.Init.Byte.xe1,$_typeof_Coq.Init.Byte.xe2,$_typeof_Coq.Init.Byte.xe3,$_typeof_Coq.Init.Byte.xe4,$_typeof_Coq.Init.Byte.xe5,$_typeof_Coq.Init.Byte.xe6,$_typeof_Coq.Init.Byte.xe7,$_typeof_Coq.Init.Byte.xe8,$_typeof_Coq.Init.Byte.xe9,$_typeof_Coq.Init.Byte.xea,$_typeof_Coq.Init.Byte.xeb,$_typeof_Coq.Init.Byte.xec,$_typeof_Coq.Init.Byte.xed,$_typeof_Coq.Init.Byte.xee,$_typeof_Coq.Init.Byte.xef,$_typeof_Coq.Init.Byte.xf0,$_typeof_Coq.Init.Byte.xf1,$_typeof_Coq.Init.Byte.xf2,$_typeof_Coq.Init.Byte.xf3,$_typeof_Coq.Init.Byte.xf4,$_typeof_Coq.Init.Byte.xf5,$_typeof_Coq.Init.Byte.xf6,$_typeof_Coq.Init.Byte.xf7,$_typeof_Coq.Init.Byte.xf8,$_typeof_Coq.Init.Byte.xf9,$_typeof_Coq.Init.Byte.xfa,$_typeof_Coq.Init.Byte.xfb,$_typeof_Coq.Init.Byte.xfc,$_typeof_Coq.Init.Byte.xfd,$_typeof_Coq.Init.Byte.xfe,$_typeof_Coq.Init.Byte.xff,$_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.IDProp,$_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.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.sum,$_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.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.sqrt,$_typeof_Coq.Init.Nat.sqrt_iter,$_typeof_Coq.Init.Nat.sub,$_typeof_Coq.Init.Nat.testbit,$_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.inleft,$_typeof_Coq.Init.Specif.inright,$_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.Init.Specif.sumor,$_typeof_Coq.Init.Wf.well_founded,$_typeof_Coq.Lists.List.In,$_typeof_Coq.Lists.List.fold_left,$_typeof_Coq.Lists.List.fold_right,$_typeof_Coq.Lists.List.last,$_typeof_Coq.Lists.List.map,$_typeof_Coq.Lists.List.nth,$_typeof_Coq.Lists.SetoidList.compat_bool,$_typeof_Coq.Lists.SetoidList.compat_op,$_typeof_Coq.Lists.SetoidList.transpose,$_typeof_Coq.Logic.Decidable.decidable,$_typeof_Coq.Logic.EqdepFacts.Eq_dep_eq_on,$_typeof_Coq.Logic.EqdepFacts.Eq_rect_eq,$_typeof_Coq.Logic.EqdepFacts.Eq_rect_eq_on,$_typeof_Coq.Logic.EqdepFacts.Streicher_K_on_,$_typeof_Coq.Logic.EqdepFacts.UIP_,$_typeof_Coq.Logic.EqdepFacts.UIP_on_,$_typeof_Coq.Logic.EqdepFacts.UIP_refl_on_,$_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.lt,$_typeof_Coq.NArith.BinNatDef.N.add,$_typeof_Coq.NArith.BinNatDef.N.compare,$_typeof_Coq.NArith.BinNatDef.N.div,$_typeof_Coq.NArith.BinNatDef.N.div2,$_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.log2,$_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.pow,$_typeof_Coq.NArith.BinNatDef.N.pred,$_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.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.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.iter,$_typeof_Coq.PArith.BinPosDef.Pos.iter_op,$_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,$_typeof_Coq.PArith.BinPosDef.Pos.sub,$_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.Qmake,$_typeof_Coq.QArith.QArith_base.Qnum,$_typeof_Coq.Reals.RIneq.Rsqr,$_typeof_Coq.Reals.RIneq.nonzeroreal,$_typeof_Coq.Reals.Rdefinitions.IZR,$_typeof_Coq.Reals.Rdefinitions.R,$_typeof_Coq.Reals.Rdefinitions.R0,$_typeof_Coq.Reals.Rdefinitions.Rdiv,$_typeof_Coq.Reals.Rdefinitions.Rge,$_typeof_Coq.Reals.Rdefinitions.Rgt,$_typeof_Coq.Reals.Rdefinitions.Rinv,$_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.Rdefinitions.up,$_typeof_Coq.Reals.Rfunctions.Z_spec,$_typeof_Coq.Reals.Rfunctions.ZintNull,$_typeof_Coq.Reals.Rfunctions.intP,$_typeof_Coq.Reals.Rpow_def.pow,$_typeof_Coq.Relations.Relation_Definitions.relation,$_typeof_Coq.Setoids.Setoid.Setoid_Theory,$_typeof_Coq.Strings.Ascii.ascii,$_typeof_Coq.Strings.String.EmptyString,$_typeof_Coq.Strings.String.String,$_typeof_Coq.Strings.String.string,$_typeof_Coq.Structures.OrderedType.Compare,$_typeof_Coq.Structures.OrderedType.EQ,$_typeof_Coq.Structures.OrderedType.GT,$_typeof_Coq.Structures.OrderedType.LT,$_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_dec,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$_typeof_Coq.Structures.OrdersTac.OEQ,$_typeof_Coq.Structures.OrdersTac.OLE,$_typeof_Coq.Structures.OrdersTac.OLT,$_typeof_Coq.Structures.OrdersTac.ord,$_typeof_Coq.Vectors.Fin.F1,$_typeof_Coq.Vectors.Fin.t,$_typeof_Coq.Vectors.VectorDef.cons,$_typeof_Coq.Vectors.VectorDef.fold_right,$_typeof_Coq.Vectors.VectorDef.nil,$_typeof_Coq.Vectors.VectorDef.t,$_typeof_Coq.ZArith.BinInt.Z.Bezout,$_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.le,$_typeof_Coq.ZArith.BinInt.Z.lt,$_typeof_Coq.ZArith.BinInt.Zne,$_typeof_Coq.ZArith.BinIntDef.Z.abs,$_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.gcd,$_typeof_Coq.ZArith.BinIntDef.Z.leb,$_typeof_Coq.ZArith.BinIntDef.Z.log2,$_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.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.rem,$_typeof_Coq.ZArith.BinIntDef.Z.sgn,$_typeof_Coq.ZArith.BinIntDef.Z.sqrt,$_typeof_Coq.ZArith.BinIntDef.Z.sub,$_typeof_Coq.ZArith.BinIntDef.Z.succ,$_typeof_Coq.ZArith.BinIntDef.Z.to_pos,$_typeof_Coq.ZArith.Zbool.Zeq_bool,$_typeof_Coq.ZArith.Zdiv.Remainder,$_typeof_Coq.ZArith.Znumtheory.Euclid,$_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs,$_typeof_Coq.micromega.Env.Env,$_typeof_Coq.micromega.Env.jump,$_typeof_Coq.micromega.Env.nth,$_typeof_Coq.micromega.EnvRing.Mon,$_typeof_Coq.micromega.EnvRing.PEX,$_typeof_Coq.micromega.EnvRing.PEadd,$_typeof_Coq.micromega.EnvRing.PEc,$_typeof_Coq.micromega.EnvRing.PEmul,$_typeof_Coq.micromega.EnvRing.PEopp,$_typeof_Coq.micromega.EnvRing.PEpow,$_typeof_Coq.micromega.EnvRing.PEsub,$_typeof_Coq.micromega.EnvRing.PExpr,$_typeof_Coq.micromega.EnvRing.PX,$_typeof_Coq.micromega.EnvRing.Pc,$_typeof_Coq.micromega.EnvRing.Pinj,$_typeof_Coq.micromega.EnvRing.Pol,$_typeof_Coq.micromega.EnvRing.mon0,$_typeof_Coq.micromega.EnvRing.vmon,$_typeof_Coq.micromega.EnvRing.zmon,$_typeof_Coq.micromega.Refl.make_conj,$_typeof_Coq.micromega.Refl.make_impl,$_typeof_Coq.micromega.RingMicromega.Formula,$_typeof_Coq.micromega.RingMicromega.Op1,$_typeof_Coq.micromega.RingMicromega.Op2,$_typeof_Coq.micromega.RingMicromega.PolEnv,$_typeof_Coq.micromega.RingMicromega.eval_op2,$_typeof_Coq.micromega.Tauto.GFormula,$_typeof_Coq.micromega.ZMicromega.Vars.Facts.Add,$_typeof_Coq.setoid_ring.Field_theory.FEX,$_typeof_Coq.setoid_ring.Field_theory.FEc,$_typeof_Coq.setoid_ring.Field_theory.FEinv,$_typeof_Coq.setoid_ring.Field_theory.FEmul,$_typeof_Coq.setoid_ring.Field_theory.FEopp,$_typeof_Coq.setoid_ring.Field_theory.FExpr,$_typeof_Coq.setoid_ring.Field_theory.Fapp,$_typeof_Coq.setoid_ring.Field_theory.condition,$_typeof_Coq.setoid_ring.Field_theory.denum,$_typeof_Coq.setoid_ring.Field_theory.linear,$_typeof_Coq.setoid_ring.Field_theory.mk_linear,$_typeof_Coq.setoid_ring.Field_theory.num,$_typeof_Coq.setoid_ring.Field_theory.rsplit,$_typeof_Coq.setoid_ring.Field_theory.rsplit_left,$_typeof_Coq.setoid_ring.Field_theory.rsplit_right,$_typeof_Coq.setoid_ring.InitialRing.Nopp,$_typeof_Coq.setoid_ring.InitialRing.Nsub,$_typeof_Coq.setoid_ring.InitialRing.gen_phiN,$_typeof_Coq.setoid_ring.InitialRing.gen_phiZ,$_typeof_Coq.setoid_ring.InitialRing.triv_div,$_typeof_Coq.setoid_ring.Ring.bool_eq,$_typeof_Coq.setoid_ring.Ring_polynom.Mon,$_typeof_Coq.setoid_ring.Ring_polynom.PEI,$_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.PEc,$_typeof_Coq.setoid_ring.Ring_polynom.PEeval,$_typeof_Coq.setoid_ring.Ring_polynom.PEmul,$_typeof_Coq.setoid_ring.Ring_polynom.PEopp,$_typeof_Coq.setoid_ring.Ring_polynom.PEpow,$_typeof_Coq.setoid_ring.Ring_polynom.PEsub,$_typeof_Coq.setoid_ring.Ring_polynom.PExpr,$_typeof_Coq.setoid_ring.Ring_polynom.PX,$_typeof_Coq.setoid_ring.Ring_polynom.Pc,$_typeof_Coq.setoid_ring.Ring_polynom.Peq,$_typeof_Coq.setoid_ring.Ring_polynom.Pinj,$_typeof_Coq.setoid_ring.Ring_polynom.Pol,$_typeof_Coq.setoid_ring.Ring_tac.ring_subst_niter,$_typeof_Coq.setoid_ring.Ring_theory.Abstract,$_typeof_Coq.setoid_ring.Ring_theory.Computational,$_typeof_Coq.setoid_ring.Ring_theory.IDphi,$_typeof_Coq.setoid_ring.Ring_theory.Morphism,$_typeof_Coq.setoid_ring.Ring_theory.SRopp,$_typeof_Coq.setoid_ring.Ring_theory.SRsub,$_typeof_Coq.setoid_ring.Ring_theory.get_sign_None,$_typeof_Coq.setoid_ring.Ring_theory.id_phi_N,$_typeof_Coq.setoid_ring.Ring_theory.pow_N,$_typeof_Coq.setoid_ring.Ring_theory.pow_pos,$_typeof_Coq.setoid_ring.Ring_theory.ring_kind,Coq.Arith.Between.bet_emp,Coq.Arith.Between.bet_eq,Coq.Arith.Compare_dec.not_eq,Coq.Arith.EqNat.eq_eq_nat,Coq.Arith.EqNat.eq_nat_eq,Coq.Arith.EqNat.eq_nat_refl,Coq.Arith.Gt.gt_le_S,Coq.Arith.Le.le_S_n,Coq.Arith.Lt.le_lt_or_eq,Coq.Arith.Lt.lt_n_S,Coq.Arith.Lt.nat_total_order,Coq.Arith.Lt.neq_0_lt,Coq.Arith.PeanoNat.Nat.Private_OrderTac.IsTotal.lt_total,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_lt,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.eq_trans,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.le_neq_lt,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_refl,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.neq_sym,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.eq_trans,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.neq_eq,Coq.Arith.PeanoNat.Nat.Private_Tac.neq_sym,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_comm,Coq.Arith.PeanoNat.Nat.add_le_mono,Coq.Arith.PeanoNat.Nat.add_le_mono_l,Coq.Arith.PeanoNat.Nat.add_wd,Coq.Arith.PeanoNat.Nat.eq_equiv,Coq.Arith.PeanoNat.Nat.eq_le_incl,Coq.Arith.PeanoNat.Nat.eq_stepl,Coq.Arith.PeanoNat.Nat.gcd_comm,Coq.Arith.PeanoNat.Nat.le_0_l,Coq.Arith.PeanoNat.Nat.le_antisymm,Coq.Arith.PeanoNat.Nat.le_gt_cases,Coq.Arith.PeanoNat.Nat.le_preorder,Coq.Arith.PeanoNat.Nat.le_stepl,Coq.Arith.PeanoNat.Nat.le_stepr,Coq.Arith.PeanoNat.Nat.le_succ_l,Coq.Arith.PeanoNat.Nat.le_trans,Coq.Arith.PeanoNat.Nat.le_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_eq_cases,Coq.Arith.PeanoNat.Nat.lt_le_incl,Coq.Arith.PeanoNat.Nat.lt_le_trans,Coq.Arith.PeanoNat.Nat.lt_stepl,Coq.Arith.PeanoNat.Nat.lt_stepr,Coq.Arith.PeanoNat.Nat.lt_succ_diag_r,Coq.Arith.PeanoNat.Nat.lt_succ_r,Coq.Arith.PeanoNat.Nat.lt_total,Coq.Arith.PeanoNat.Nat.lt_trichotomy,Coq.Arith.PeanoNat.Nat.lt_wd,Coq.Arith.PeanoNat.Nat.max_l,Coq.Arith.PeanoNat.Nat.max_r,Coq.Arith.PeanoNat.Nat.min_l,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_1_r,Coq.Arith.PeanoNat.Nat.mul_assoc,Coq.Arith.PeanoNat.Nat.mul_cancel_l,Coq.Arith.PeanoNat.Nat.mul_comm,Coq.Arith.PeanoNat.Nat.mul_wd,Coq.Arith.PeanoNat.Nat.neq_0_lt_0,Coq.Arith.PeanoNat.Nat.neq_sym,Coq.Arith.PeanoNat.Nat.one_succ,Coq.Arith.PeanoNat.Nat.pow_nonzero,Coq.Arith.PeanoNat.Nat.pred_succ,Coq.Arith.PeanoNat.Nat.succ_wd,Coq.Arith.PeanoNat.Nat.two_succ,Coq.Bool.Bool.Is_true_eq_left,Coq.Bool.Bool.Is_true_eq_right,Coq.Bool.Bool.andb_true_r,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_false_abs,Coq.Bool.Bool.eq_true_iff_eq,Coq.Bool.Bool.not_false_is_true,Coq.Bool.Bool.not_true_is_false,Coq.Bool.Bool.orb_true_intro,Coq.Bool.Bool.trans_eq_bool,Coq.Init.Datatypes.comparison_eq_stable,Coq.Init.Datatypes.list_ind,Coq.Init.Datatypes.nat_ind,Coq.Init.Peano.f_equal2_nat,Coq.Init.Peano.f_equal_nat,Coq.Init.Peano.le_S,Coq.Init.Peano.le_n,Coq.Init.Peano.not_eq_S,Coq.Init.Specif.proj2_sig,Coq.Init.Wf.Acc_inv,Coq.Lists.List.map_ext,Coq.Logic.Decidable.dec_not_not,Coq.Logic.Decidable.not_not_iff,Coq.Logic.EqdepFacts.UIP_shift_on,Coq.Logic.EqdepFacts.eq_dep1_intro,Coq.Logic.EqdepFacts.eq_dep_intro,Coq.Logic.EqdepFacts.eq_indd,Coq.Logic.EqdepFacts.internal_eq_sym_internal,Coq.Logic.Eqdep_dec.K_dec,Coq.Logic.Eqdep_dec.K_dec_on,Coq.Logic.Eqdep_dec.UIP_dec,Coq.Logic.Eqdep_dec.eq_dep_eq_dec,Coq.Logic.Eqdep_dec.eq_proofs_unicity,Coq.Logic.Eqdep_dec.eq_proofs_unicity_on,Coq.NArith.BinNat.N.Private_OrderTac.IsTotal.lt_total,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.eq_trans,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.le_neq_lt,Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_refl,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.neq_sym,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.eq_trans,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.neq_eq,Coq.NArith.BinNat.N.Private_Tac.neq_sym,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_comm,Coq.NArith.BinNat.N.eq_equiv,Coq.NArith.BinNat.N.eq_le_incl,Coq.NArith.BinNat.N.eq_stepl,Coq.NArith.BinNat.N.le_0_l,Coq.NArith.BinNat.N.le_gt_cases,Coq.NArith.BinNat.N.le_preorder,Coq.NArith.BinNat.N.le_stepl,Coq.NArith.BinNat.N.le_stepr,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_eq_cases,Coq.NArith.BinNat.N.lt_le_trans,Coq.NArith.BinNat.N.lt_stepl,Coq.NArith.BinNat.N.lt_stepr,Coq.NArith.BinNat.N.lt_succ_diag_r,Coq.NArith.BinNat.N.lt_total,Coq.NArith.BinNat.N.lt_trichotomy,Coq.NArith.BinNat.N.mul_0_l,Coq.NArith.BinNat.N.mul_1_l,Coq.NArith.BinNat.N.mul_assoc,Coq.NArith.BinNat.N.mul_cancel_l,Coq.NArith.BinNat.N.mul_comm,Coq.NArith.BinNat.N.neq_0_lt_0,Coq.NArith.BinNat.N.neq_sym,Coq.NArith.BinNat.N.one_succ,Coq.NArith.BinNat.N.pow_nonzero,Coq.NArith.BinNat.N.pred_succ,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.eq_trans,Coq.PArith.BinPos.Pos.Private_Tac.le_antisym,Coq.PArith.BinPos.Pos.Private_Tac.le_neq_lt,Coq.PArith.BinPos.Pos.Private_Tac.lt_irrefl,Coq.PArith.BinPos.Pos.Private_Tac.neq_eq,Coq.PArith.BinPos.Pos.Private_Tac.neq_sym,Coq.PArith.BinPos.Pos.Private_Tac.not_neq_eq,Coq.PArith.BinPos.Pos.eq_equiv,Coq.PArith.BinPos.Pos.iter_swap_gen,Coq.PArith.BinPos.Pos.lt_total,Coq.PArith.Pnat.Pos2Nat.inj,Coq.QArith.QArith_base.Q_Setoid,Coq.Reals.DiscrR.IZR_eq,Coq.Reals.RIneq.IZR_neq,Coq.Reals.RIneq.Rdichotomy,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_le,Coq.Reals.RIneq.Rgt_eq_compat,Coq.Reals.RIneq.Rlt_eq_compat,Coq.Reals.RIneq.Rlt_irrefl,Coq.Reals.RIneq.Rlt_le,Coq.Reals.RIneq.Rmult_eq_compat_l,Coq.Reals.RIneq.Rmult_eq_compat_r,Coq.Reals.RIneq.Ropp_eq_compat,Coq.Reals.RIneq.Ropp_involutive,Coq.Reals.RIneq.Rplus_eq_compat_l,Coq.Reals.RIneq.Rplus_eq_compat_r,Coq.Reals.RIneq.eq_IZR,Coq.Reals.RIneq.f_equal_R,Coq.Reals.Raxioms.Rmult_comm,Coq.Setoids.Setoid.Seq_refl,Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_sym,Coq.ZArith.BinInt.Z.Private_OrderTac.IsTotal.lt_total,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_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.eq_trans,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.neq_eq,Coq.ZArith.BinInt.Z.Private_Tac.neq_sym,Coq.ZArith.BinInt.Z.Private_Tac.not_neq_eq,Coq.ZArith.BinInt.Z.abs_eq,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,Coq.ZArith.BinInt.Z.add_le_mono_l,Coq.ZArith.BinInt.Z.add_le_mono_r,Coq.ZArith.BinInt.Z.add_lt_mono_l,Coq.ZArith.BinInt.Z.add_shuffle0,Coq.ZArith.BinInt.Z.add_shuffle1,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_opp_l,Coq.ZArith.BinInt.Z.eq_opp_r,Coq.ZArith.BinInt.Z.eq_stepl,Coq.ZArith.BinInt.Z.eq_sym_iff,Coq.ZArith.BinInt.Z.gcd_comm,Coq.ZArith.BinInt.Z.gt_lt,Coq.ZArith.BinInt.Z.le_antisymm,Coq.ZArith.BinInt.Z.le_decidable,Coq.ZArith.BinInt.Z.le_ge_cases,Coq.ZArith.BinInt.Z.le_gt_cases,Coq.ZArith.BinInt.Z.le_lt_trans,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_succ_l,Coq.ZArith.BinInt.Z.le_trans,Coq.ZArith.BinInt.Z.le_wd,Coq.ZArith.BinInt.Z.lt_0_1,Coq.ZArith.BinInt.Z.lt_1_2,Coq.ZArith.BinInt.Z.lt_ge_cases,Coq.ZArith.BinInt.Z.lt_le_incl,Coq.ZArith.BinInt.Z.lt_le_trans,Coq.ZArith.BinInt.Z.lt_stepl,Coq.ZArith.BinInt.Z.lt_stepr,Coq.ZArith.BinInt.Z.lt_succ_r,Coq.ZArith.BinInt.Z.lt_total,Coq.ZArith.BinInt.Z.lt_trichotomy,Coq.ZArith.BinInt.Z.max_l,Coq.ZArith.BinInt.Z.max_r,Coq.ZArith.BinInt.Z.max_spec,Coq.ZArith.BinInt.Z.min_l,Coq.ZArith.BinInt.Z.min_r,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_assoc,Coq.ZArith.BinInt.Z.mul_cancel_l,Coq.ZArith.BinInt.Z.mul_comm,Coq.ZArith.BinInt.Z.mul_nonneg_nonneg,Coq.ZArith.BinInt.Z.mul_opp_l,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_shuffle3,Coq.ZArith.BinInt.Z.neq_sym,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_nonneg_nonpos,Coq.ZArith.BinInt.Z.opp_pos_neg,Coq.ZArith.BinInt.Z.sgn_null,Coq.ZArith.BinInt.Z.sub_0_r,Coq.ZArith.BinInt.Z.sub_diag,Coq.ZArith.BinInt.Z.succ_pred,Coq.ZArith.BinInt.Z_eq_mult,Coq.ZArith.BinInt.Zeq_minus,Coq.ZArith.BinInt.Zplus_eq_compat,Coq.ZArith.BinInt.Zpos_eq,Coq.ZArith.BinInt.Zsucc_eq_compat,Coq.ZArith.Zcompare.Zcompare_eq_case,Coq.ZArith.Zorder.Znot_le_gt,Coq.ZArith.Zorder.not_Zeq,Coq.ZArith.auxiliary.Zegal_left,Coq.ZArith.auxiliary.Zle_left,Coq.micromega.EnvRing.Mphi_morph,Coq.micromega.EnvRing.env_morph,Coq.micromega.RingMicromega.cleb_sound,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.E_ST,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.Equal_ST,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.In_eq_iff,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.dec_eq,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.eq_refl_iff,Coq.omega.OmegaLemmas.OMEGA1,Coq.omega.OmegaLemmas.OMEGA2,Coq.omega.OmegaLemmas.OMEGA5,Coq.omega.OmegaLemmas.OMEGA6,Coq.omega.OmegaLemmas.OMEGA8,Coq.omega.OmegaLemmas.new_var,Coq.omega.PreOmega.Z.div_0_r_ext,Coq.omega.PreOmega.Z.mod_0_r_ext,Coq.omega.PreOmega.Z.quot_0_r_ext,Coq.omega.PreOmega.Z.rem_0_r_ext,Coq.setoid_ring.Field_theory.AF_AR,Coq.setoid_ring.Field_theory.rmul_ext_Proper,Coq.setoid_ring.InitialRing.gen_phiZ_ext,Coq.setoid_ring.Ring_theory.ARdistr_r,Coq.setoid_ring.Ring_theory.ARmul_0_l,Coq.setoid_ring.Ring_theory.ARmul_0_r,Coq.setoid_ring.Ring_theory.ARmul_1_l,Coq.setoid_ring.Ring_theory.ARmul_1_r,Coq.setoid_ring.Ring_theory.ARmul_assoc,Coq.setoid_ring.Ring_theory.ARmul_comm,Coq.setoid_ring.Ring_theory.ARopp_mul_l,Coq.setoid_ring.Ring_theory.ARopp_zero,Coq.setoid_ring.Ring_theory.ARsub_def,Coq.setoid_ring.Ring_theory.Eq_ext,Coq.setoid_ring.Ring_theory.Eq_s_ext,Coq.setoid_ring.Ring_theory.Eqsth,Coq.setoid_ring.Ring_theory.Rth_ARth,Coq.setoid_ring.Ring_theory.Smorph0,Coq.setoid_ring.Ring_theory.Smorph_add,Coq.setoid_ring.Ring_theory.mk_reqe,Coq.setoid_ring.Ring_theory.morph0,Coq.setoid_ring.Ring_theory.morph1,Coq.setoid_ring.Ring_theory.morph_add,Coq.setoid_ring.Ring_theory.morph_eq,Coq.setoid_ring.Ring_theory.morph_mul,Coq.setoid_ring.Ring_theory.morph_opp,Coq.setoid_ring.Ring_theory.morph_sub,Coq.setoid_ring.Ring_theory.rpow_pow_N,$adef_Coq.PArith.BinPos.Pos.SqrtSpec_$a2,$adef_Coq.Arith.PeanoNat.Nat.eqf_$a2,$adef_Coq.setoid_ring.Ring_theory.SRopp_$a1,$adef_Coq.Reals.Rdefinitions.IZR_$a1,$adef_Coq.Init.Datatypes.None_$a1,$adef_Coq.NArith.BinNat.N.lt_$a2,$adef_Coq.ZArith.BinIntDef.Z.of_N_$a1,$adef_Coq.Vectors.VectorDef.cons_$a4,$adef_Coq.ZArith.BinIntDef.Z.modulo_$a2,$adef_Coq.Init.Datatypes.BoolSpec_$a3,$adef_Coq.setoid_ring.Ring_theory.SRopp_$a2,$adef_Coq.PArith.BinPosDef.Pos.of_nat_$a1,$adef_Coq.Reals.Rfunctions.ZintPos_$a2,$adef_Coq.setoid_ring.Ring_theory.sring_eq_ext_$a4,$adef_Coq.setoid_ring.Ring_theory.get_sign_None_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEc_$a2,$adef_Coq.micromega.EnvRing.Pol_$a1,$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.Init.Nat.even_$a1,$adef_Coq.setoid_ring.Ring_polynom.vmon_$a2,$adef_Coq.NArith.BinNatDef.N.div_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.Exists_$a2,$adef_Coq.setoid_ring.BinList.nth_$a4,$adef_$_fix_20500_1_add_carry_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pol_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.mem_$a2,$adef_$_lam_14771_$a2,$adef_Coq.Reals.Rdefinitions.IPR_$a1,$adef_Coq.micromega.Env.Env_$a1,$adef_Coq.Init.Datatypes.CompareSpecT_$a4,$adef_Coq.ZArith.BinIntDef.Z.pred_$a1,$adef_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_elt_Prop_$a1,$adef_Coq.setoid_ring.Field_theory.FEdiv_$a3,$adef_Coq.Init.Nat.compare_$a2,$adef_Coq.setoid_ring.Ring_theory.almost_ring_theory_$a8,$adef_Coq.Logic.EqdepFacts.Eq_rect_eq_$a1,$adef_Coq.Init.Specif.projT2_$a3,$adef_Coq.Init.Datatypes.app_$a3,$adef_Coq.setoid_ring.InitialRing.gen_phiZ_$a7,$adef_Coq.Init.Specif.existT_$a4,$adef_Coq.Init.Specif.sig_$a2,$adef_Coq.NArith.BinNatDef.N.sqrt_$a1,$adef_Coq.ZArith.BinIntDef.Z.leb_$a2,$adef_Coq.PArith.BinPosDef.Pos.pred_double_$a1,$adef_Coq.setoid_ring.Field_theory.FEmul_$a3,$adef_Coq.setoid_ring.Field_theory.Fapp_$a4,$adef_Coq.ZArith.BinIntDef.Z.mul_$a2,$adef_Coq.ZArith.BinIntDef.Z.sqrt_$a1,$adef_Coq.PArith.BinPosDef.Pos.iter_$a4,$adef_Coq.FSets.FSetPositive.PositiveSet.Equal_$a2,$adef_Coq.micromega.RingMicromega.Build_Formula_$a4,$adef_Coq.Init.Specif.sumbool_$a2,$adef_$_prop_441_$a2,$adef_Coq.setoid_ring.Field_theory.mk_rsplit_$a4,$adef_Coq.Lists.List.last_$a3,$adef_Coq.Init.Specif.proj1_sig_$a3,$adef_Coq.Init.Nat.div_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEsub_$a3,$adef_Coq.Init.Nat.max_$a2,$adef_$_lam_14795_$a4,$adef_Coq.PArith.BinPosDef.Pos.pred_N_$a1,$adef_Coq.Structures.OrderedTypeEx.Z_as_OT.lt_$a2,$adef_Coq.Init.Datatypes.option_$a1,$adef_Coq.Relations.Relation_Definitions.relation_$a1,$adef_$_prop_23385_$a3,$adef_Coq.ZArith.BinIntDef.Z.eqb_$a2,$adef_Coq.NArith.BinNatDef.N.sub_$a2,$adef_Coq.setoid_ring.Ring_polynom.Peq_$a4,$adef_Coq.Structures.OrderedType.LT_$a5,$adef_$_lam_14779_$a2,$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_$_prop_440_$a2,$adef_Coq.micromega.RingMicromega.SORaddon_$a22,$adef_Coq.ZArith.Zpower.two_power_pos_$a1,$adef_$_prop_23380_$a4,$adef_Coq.setoid_ring.Field_theory.FExpr_$a1,$adef_Coq.micromega.RingMicromega.PolEnv_$a1,$adef_Coq.NArith.BinNat.N.b2n_$a1,$adef_Coq.Logic.EqdepFacts.UIP__$a1,$adef_Coq.Reals.Rdefinitions.Rle_$a2,$adef_$_lam_14787_$a2,$adef_$_case_Coq.Init.Datatypes.prod$8582_$a9,$adef_Coq.micromega.EnvRing.zmon_$a2,$adef_Coq.Bool.Zerob.zerob_$a1,$adef_Coq.PArith.BinPosDef.Pos.pred_$a1,$adef_Coq.Logic.EqdepFacts.eq_dep_$a6,$adef_Coq.Init.Nat.eqb_$a2,$adef_Coq.setoid_ring.Ring_theory.div_theory_$a7,$adef_Coq.Reals.Rfunctions.Z_spec_$a2,$adef_Coq.Init.Datatypes.inl_$a3,$adef_Coq.NArith.BinNat.N.divide_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_eq_ext_$a5,$adef_Coq.Logic.EqdepFacts.Streicher_K_on__$a3,$adef_Coq.Logic.EqdepFacts.Eq_dep_eq_on_$a4,$adef_Coq.setoid_ring.Ring.bool_eq_$a2,$adef_Coq.ZArith.BinInt.Z.b2z_$a1,$adef_Coq.Reals.Rdefinitions.Rdiv_$a2,$adef_Coq.Init.Datatypes.nil_$a1,$adef_Coq.Logic.EqdepFacts.eq_dep1_$a6,$adef_Coq.NArith.BinNatDef.N.max_$a2,$adef_Coq.Reals.Rdefinitions.Rge_$a2,$adef_Coq.Init.Datatypes.CompGtT_$a3,$adef_Coq.setoid_ring.Field_theory.rsplit_left_$a2,$adef_Coq.Reals.Rdefinitions.Rmult_$a2,$adef_Coq.Reals.Rfunctions.ZintNeg_$a2,$adef_Coq.Init.Datatypes.CompareSpecT_$a3,$adef_$_lam_14779_$a4,$adef_Coq.micromega.Tauto.GFormula_$a4,$adef_Coq.ZArith.Znumtheory.Bezout_$a3,$adef_Coq.Numbers.BinNums.Npos_$a1,$adef_Coq.setoid_ring.Ring_theory.Morphism_$a17,$adef_Coq.setoid_ring.Ring_theory.IDphi_$a2,$adef_Coq.micromega.Env.jump_$a4,$adef_$_case_Coq.Init.Datatypes.bool$102739_$a2,$adef_Coq.setoid_ring.Ring_theory.SRsub_$a2,$adef_Coq.Numbers.BinNums.xI_$a1,$adef_Coq.Logic.EqdepFacts.UIP_refl_on__$a1,$adef_Coq.setoid_ring.Field_theory.condition_$a2,$adef_Coq.ZArith.BinIntDef.Z.to_pos_$a1,$adef_$_case_Coq.Init.Datatypes.bool$142229_$a4,$adef_Coq.Init.Nat.div2_$a1,$adef_Coq.Init.Datatypes.negb_$a1,$adef_Coq.Init.Nat.testbit_$a2,$adef_$_lam_12266_$a1,$adef_Coq.Reals.Rdefinitions.Ropp_$a1,$adef_Coq.setoid_ring.Ring_polynom.PEeval_$a14,$adef_Coq.Init.Datatypes.nat_rect_$a3,$adef_Coq.Arith.Even.odd_$a1,$adef_Coq.ZArith.BinIntDef.Z.succ_$a1,$adef_$_lam_14795_$a2,$adef_Coq.Init.Nat.add_$a2,$adef_Coq.Init.Specif.sigT2_$a3,$adef_Coq.Structures.OrderedType.Compare_$a5,$adef_Coq.setoid_ring.Field_theory.FEc_$a2,$adef_Coq.Classes.Morphisms.Proper_$a3,$adef_Coq.Reals.Rdefinitions.Rminus_$a2,$adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2,$adef_Coq.Init.Specif.right_$a2,$adef_Coq.setoid_ring.Ring_theory.power_theory_$a7,$adef_Coq.Init.Logic.eq_refl_$a2,$adef_Coq.Lists.List.fold_left_$a5,$adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3,$adef_Coq.Sorting.Sorted.StronglySorted_$a3,$adef_Coq.Reals.Rdefinitions.Rplus_$a2,$adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2,$adef_Coq.setoid_ring.Field_theory.FEadd_$a3,$adef_Coq.PArith.BinPosDef.Pos.sqrt_$a1,$adef_Coq.Init.Datatypes.S_$a1,$adef_Coq.Strings.Ascii.Ascii_$a8,$adef_Coq.micromega.EnvRing.PEpow_$a3,$adef_Coq.setoid_ring.Ring_polynom.zmon_$a2,$adef_Coq.setoid_ring.Ring_theory.semi_morph_$a13,$adef_Coq.ZArith.BinIntDef.Z.add_$a2,$adef_Coq.micromega.RingMicromega.Formula_$a1,$adef_Coq.setoid_ring.Ring_theory.SRsub_$a4,$adef_$_prop_23386_$a2,$adef_$_case_Coq.Init.Datatypes.comparison$165612_$a5,$adef_Coq.Lists.SetoidList.InA_$a4,$adef_Coq.setoid_ring.Field_theory.num_$a2,$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.Field_theory.mk_linear_$a4,$adef_$_case_Coq.Numbers.BinNums.Z$21828_$a3,$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.BinInt.Z.gt_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEO_$a1,$adef_Coq.Init.Logic.eq_rect_$a5,$adef_Coq.Numbers.BinNums.xO_$a1,$adef_$_case_Coq.Init.Datatypes.nat$21811_$a3,$adef_Coq.ZArith.Zdiv.Remainder_$a2,$adef_Coq.Reals.Rdefinitions.Rinv_$a1,$adef_Coq.setoid_ring.Field_theory.FEinv_$a2,$adef_Coq.ZArith.Zpower.Zdiv_rest_proof_$a4,$adef_Coq.Init.Wf.Acc_$a3,$adef_Coq.setoid_ring.Ring_theory.pow_N_$a5,$adef_Coq.ZArith.BinInt.Z.ge_$a2,$adef_Coq.ZArith.Zbool.Zeq_bool_$a2,$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.Init.Nat.sqrt_$a1,$adef_Coq.Init.Datatypes.sum_$a2,$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.InitialRing.triv_div_$a6,$adef_Coq.Vectors.Fin.t_$a1,$adef_Coq.setoid_ring.Field_theory.FEO_$a1,$adef_$_let_var_6_p_21876_21878_$a4,$adef_Coq.Lists.List.In_$a3,$adef_Coq.Vectors.VectorDef.fold_right_$a6,$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.FSets.FSetPositive.PositiveSet.Node_$a3,$adef_Coq.Arith.PeanoNat.Nat.divide_$a2,$adef_Coq.setoid_ring.Field_theory.rsplit_$a1,$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.micromega.EnvRing.PEmul_$a3,$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.Init.Datatypes.CompLtT_$a3,$adef_Coq.Lists.List.nth_$a4,$adef_Coq.Lists.SetoidList.transpose_$a4,$adef_Coq.micromega.EnvRing.Pphi_$a7,$adef_Coq.Init.Datatypes.inr_$a3,$adef_Coq.micromega.RingMicromega.eval_op2_$a5,$adef_$_prop_10582_$a3,$adef_$_prop_20885_$a2,$adef_Coq.Vectors.Fin.F1_$a1,$adef_Coq.QArith.QArith_base.Qnum_$a1,$adef_Coq.NArith.BinNatDef.N.succ_double_$a1,$adef_Coq.PArith.BinPosDef.Pos.succ_$a1,$adef_Coq.setoid_ring.Field_theory.FEsub_$a3,$adef_Coq.micromega.Tauto.D_$a6,$adef_Coq.Init.Datatypes.prod_$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.setoid_ring.InitialRing.gen_phiPOS_$a5,$adef_Coq.NArith.BinNatDef.N.div2_$a1,$adef_Coq.Strings.Ascii.nat_of_ascii_$a1,$adef_Coq.NArith.BinNatDef.N.gcd_$a2,$adef_Coq.micromega.Env.nth_$a3,$adef_$_prop_23382_$a3,$adef_Coq.Bool.Bool.eqb_$a2,$adef_Coq.NArith.BinNatDef.N.div_eucl_$a2,$adef_Coq.Lists.SetoidList.compat_op_$a5,$adef_Coq.ZArith.BinInt.Z.lt_$a2,$adef_Coq.setoid_ring.Field_theory.linear_$a1,$adef_Coq.Init.Nat.gcd_$a2,$adef_Coq.Arith.PeanoNat.Nat.b2n_$a1,$adef_Coq.PArith.BinPosDef.Pos.eqb_$a2,$adef_Coq.Structures.OrderedTypeEx.String_as_OT.lts_$a2,$adef_$_case_Coq.Init.Datatypes.nat$21833_$a1,$adef_Coq.ZArith.BinIntDef.Z.opp_$a1,$adef_Coq.Numbers.BinNums.Zneg_$a1,$adef_Coq.Reals.Rdefinitions.Rgt_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3,$adef_Coq.NArith.BinNatDef.N.to_nat_$a1,$adef_$_lam_14771_$a4,$adef_Coq.micromega.EnvRing.Mphi_$a5,$adef_Coq.Bool.Bool.reflect_$a2,$adef_Coq.NArith.BinNatDef.N.pow_$a2,$adef_Coq.setoid_ring.Ring_polynom.PX_$a4,$adef_Coq.Arith.Between.between_$a3,$adef_Coq.PArith.BinPosDef.Pos.sub_mask_$a2,$adef_Coq.Init.Specif.inright_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEI_$a1,$adef_Coq.Logic.EqdepFacts.UIP_refl_on__$a2,$adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3,$adef_Coq.setoid_ring.Field_theory.FEopp_$a2,$adef_Coq.Init.Specif.exist2_$a4,$adef_Coq.Init.Datatypes.CompareSpec_$a4,$adef_Coq.Init.Datatypes.xorb_$a2,$adef_Coq.Strings.String.String_$a2,$adef_Coq.NArith.BinNatDef.N.modulo_$a2,$adef_Coq.ZArith.Znumtheory.Euclid_intro_$a5,$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_$_prop_32246_$a2,$adef_$_prop_10581_$a3,$adef_Coq.NArith.BinNatDef.N.succ_$a1,$adef_Coq.Structures.OrderedType.GT_$a5,$adef_Coq.setoid_ring.Ring_theory.id_phi_N_$a1,$adef_Coq.Vectors.Fin.FS_$a2,$adef_Coq.micromega.EnvRing.PExpr_$a1,$adef_Coq.Setoids.Setoid.Setoid_Theory_$a2,$adef_Coq.setoid_ring.Field_theory.rsplit_right_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.is_empty_$a1,$adef_Coq.Lists.SetoidList.NoDupA_$a3,$adef_Coq.ZArith.BinInt.Z.Bezout_$a3,$adef_Coq.Logic.EqdepFacts.UIP_on__$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.Subset_$a2,$adef_Coq.Arith.EqNat.eq_nat_$a2,$adef_$_let_var_6_p_21874_21877_$a4,$adef_Coq.micromega.Tauto.A_$a6,$adef_Coq.micromega.EnvRing.vmon_$a2,$adef_Coq.micromega.Tauto.X_$a5,$adef_Coq.setoid_ring.Field_theory.almost_field_theory_$a10,$adef_Coq.Init.Specif.sumor_$a2,$adef_Coq.ZArith.BinIntDef.Z.rem_$a2,$adef_Coq.PArith.BinPosDef.Pos.mul_$a2,$adef_Coq.PArith.BinPosDef.Pos.testbit_$a2,$adef_Coq.NArith.BinNatDef.N.mul_$a2,$adef_Coq.Init.Nat.pred_$a1,$adef_$_prop_23383_$a3,$adef_Coq.Init.Specif.exist_$a3,$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.Init.Specif.inleft_$a3,$adef_Coq.micromega.EnvRing.Pinj_$a3,$adef_Coq.ZArith.BinIntDef.Z.quot_$a2,$adef_Coq.NArith.BinNatDef.N.log2_$a1,$adef_Coq.Init.Wf.well_founded_$a2,$adef_Coq.Init.Datatypes.cons_$a3,$adef_Coq.setoid_ring.Ring_theory.Computational_$a3,$adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1,$adef_Coq.Init.Datatypes.pair_$a4,$adef_Coq.PArith.BinPosDef.Pos.IsPos_$a1,$adef_Coq.Init.Nat.sqrt_iter_$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.Structures.OrderedType.EQ_$a5,$adef_Coq.Numbers.BinNums.Zpos_$a1,$adef_Coq.NArith.BinNatDef.N.double_$a1,$adef_Coq.Init.Datatypes.list_$a1,$adef_$_prop_23384_$a3,$adef_$_lam_103102_$a1,$adef_Coq.Init.Nat.sub_$a2,$adef_Coq.PArith.BinPos.Pos.SubMaskSpec_$a3,$adef_Coq.NArith.BinNatDef.N.add_$a2,$adef_Coq.ZArith.BinInt.Z.divide_$a2,$adef_Coq.PArith.BinPosDef.Pos.gcd_$a2,$adef_Coq.Bool.Bool.ReflectF_$a1,$adef_Coq.Reals.Rfunctions.ZintNull_$a1,$adef_Coq.setoid_ring.Field_theory.FEI_$a1,$adef_Coq.micromega.EnvRing.PEX_$a2,$adef_Coq.Bool.Bool.ReflectT_$a1,$adef_Coq.ZArith.Znumtheory.Euclid_$a2,$adef_Coq.Lists.List.Forall_$a3,$adef_Coq.PArith.BinPosDef.Pos.sub_$a2,$adef_Coq.NArith.BinNatDef.N.compare_$a2,$adef_Coq.Init.Datatypes.fst_$a3,$adef_Coq.ZArith.BinIntDef.Z.quotrem_$a2,$adef_$_lam_14787_$a4,$adef_Coq.ZArith.BinIntDef.Z.min_$a2,$adef_Coq.micromega.Tauto.N_$a5,$adef_Coq.setoid_ring.InitialRing.gen_phiN_$a6,$adef_Coq.Init.Nat.min_$a2,$adef_Coq.Init.Specif.existT2_$a6,$adef_Coq.ZArith.BinInt.Zne_$a2,$adef_Coq.Reals.RIneq.Rsqr_$a1,$adef_Coq.PArith.BinPosDef.Pos.compare_$a2,$adef_Coq.Reals.RIneq.mknonzeroreal_$a1,$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_$_prop_166330_$a2,$adef_Coq.Init.Nat.odd_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.equal_$a2,$adef_Coq.setoid_ring.Ring_theory.sign_theory_$a4,$adef_Coq.NArith.BinNatDef.N.even_$a1,$adef_Coq.setoid_ring.Field_theory.FEX_$a2,$adef_Coq.Lists.List.NoDup_$a2,$adef_Coq.Vectors.VectorDef.nil_$a1,$adef_Coq.Init.Specif.left_$a2,$adef_Coq.Logic.EqdepFacts.Eq_rect_eq_on_$a4,$adef_Coq.Lists.SetoidList.compat_bool_$a3,$adef_Coq.Init.Specif.sigT_$a2,$adef_Coq.ZArith.BinIntDef.Z.pow_$a2,$adef_Coq.micromega.EnvRing.PX_$a4,$adef_Coq.micromega.EnvRing.PEadd_$a3,$adef_Coq.Init.Specif.sig2_$a3,$adef_Coq.setoid_ring.Field_theory.FEpow_$a3,$adef_Coq.Init.Datatypes.length_$a2,$adef_Coq.NArith.BinNatDef.N.eqb_$a2,$adef_Coq.NArith.BinNat.N.eqf_$a2,$adef_Coq.setoid_ring.Field_theory.denum_$a2,$adef_Coq.micromega.ZMicromega.is_diff_env_elt_$a4,$adef_$_prop_23381_$a3,$adef_Coq.NArith.BinNat.N.le_$a2,$adef_Coq.Classes.RelationClasses.PreOrder_$a2,$adef_Coq.Init.Nat.divmod_$a4,$adef_Coq.ZArith.Zpower.Zdiv_rest_proofs_$a2,$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.Init.Peano.gt_$a2,$tdef_$_type_183,$tdef_$_type_16600,$tdef_$_type_22749,$tdef_Coq.micromega.Env.Env,$tdef_$_type_6968,$tdef_Coq.ZArith.Znumtheory.Euclid,$tdef_$_type_27676,$tdef_$_type_13656,$tdef_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$tdef_$_type_30063,$tdef_$_type_550,$tdef_$_type_6134,$tdef_$_type_594,$tdef_Coq.micromega.EnvRing.Mon,$tdef_$_type_2507,$tdef_$_type_25623,$tdef_$_type_15391,$tdef_$_type_10202,$tdef_$_type_12123,$tdef_Coq.Init.Specif.sigT2,$tdef_$_type_8909,$tdef_$_type_400,$tdef_$_type_6347,$tdef_$_type_4850,$tdef_$_type_29371,$tdef_$_type_20466,$tdef_$_type_102836,$tdef_$_type_166308,$tdef_$_type_10127,$tdef_Coq.Init.Datatypes.bool,$tdef_$_type_10132,$tdef_Coq.Init.Datatypes.list,$tdef_$_type_9212,$tdef_$_type_20462,$tdef_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$tdef_$_type_7802,$tdef_Coq.Structures.OrdersTac.ord,$tdef_$_type_8427,$tdef_Coq.micromega.EnvRing.PExpr,$tdef_Coq.Init.Datatypes.option,$tdef_$_type_29419,$tdef_$_type_3227,$tdef_$_type_2135,$tdef_$_type_166325,$tdef_$_type_145287,$tdef_$_type_13882,$tdef_$_type_10221,$tdef_$_type_8469,$tdef_$_type_13213,$tdef_$_type_20153,$tdef_$_type_156173,$tdef_$_type_929,$tdef_$_type_8915,$tdef_$_type_8327,$tdef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$tdef_$_type_10101,$tdef_$_type_2076,$tdef_$_type_10200,$tdef_$_type_4,$tdef_$_type_8828,$tdef_Coq.Structures.OrderedTypeEx.N_as_OT.t,$tdef_$_type_20994,$tdef_$_type_17903,$tdef_Coq.FSets.FSetPositive.PositiveSet.elt,$tdef_$_type_5330,$tdef_$_type_18100,$tdef_$_type_18093,$tdef_$_type_405,$tdef_$_type_29456,$tdef_$_type_159221,$tdef_$_type_2493,$tdef_$_type_13651,$tdef_$_type_8139,$tdef_$_type_23408,$tdef_$_type_13638,$tdef_$_type_101786,$tdef_Coq.setoid_ring.Ring_polynom.Mon,$tdef_Coq.Init.Datatypes.comparison,$tdef_$_type_8784,$tdef_$_type_31840,$tdef_$_type_22765,$tdef_$_type_32438,$tdef_$_type_6542,$tdef_$_type_2931,$tdef_$_type_12719,$tdef_$_type_17120,$tdef_$_type_12921,$tdef_$_type_158399,$tdef_Coq.micromega.Tauto.GFormula,$tdef_Coq.Numbers.BinNums.N,$tdef_$_type_9218,$tdef_$_type_386,$tdef_Coq.Init.Specif.sig2,$tdef_$_type_31858,$tdef_$_type_29701,$tdef_$_type_11789,$tdef_$_type_397,$tdef_$_type_17856,$tdef_$_type_22,$tdef_$_type_5414,$tdef_Coq.Init.Specif.sumbool,$tdef_$_type_547,$tdef_$_type_166265,$tdef_$_type_17370,$tdef_$_type_23298,$tdef_$_type_13833,$tdef_$_type_25277,$tdef_Coq.Reals.Rdefinitions.R,$tdef_$_type_29742,$tdef_$_type_30688,$tdef_$_type_417,$tdef_$_type_32317,$tdef_$_type_6755,$tdef_$_type_25969,$tdef_$_type_12105,$tdef_$_type_10051,$tdef_$_type_8904,$tdef_$_type_31864,$tdef_$_type_158368,$tdef_$_type_15251,$tdef_$_type_145293,$tdef_$_type_10579,$tdef_$_type_32468,$tdef_$_type_7589,$tdef_$_type_9228,$tdef_$_type_2081,$tdef_$_type_22757,$tdef_$_type_17934,$tdef_Coq.setoid_ring.Field_theory.FExpr,$tdef_$_type_32412,$tdef_Coq.FSets.FSetPositive.PositiveSet.t,$tdef_$_type_23727,$tdef_Coq.Init.Datatypes.unit,$tdef_$_type_22667,$tdef_$_type_8519,$tdef_$_type_29857,$tdef_Coq.Init.Specif.sig,$tdef_$_type_29712,$tdef_$_type_155143,$tdef_$_type_7181,$tdef_$_type_5093,$tdef_$_type_32443,$tdef_Coq.Init.Datatypes.sum,$tdef_$_type_28345,$tdef_$_type_13519,$tdef_$_type_17745,$tdef_$_type_5354,$tdef_$_type_166286,$tdef_$_type_8172,$tdef_Coq.Strings.Ascii.ascii,$tdef_Coq.FSets.FSetPositive.PositiveSet.tree,$tdef_$_type_29693,$tdef_$_type_18058,$tdef_$_type_10187,$tdef_$_type_8704,$tdef_$_type_20164,$tdef_$_type_166294,$tdef_$_type_154763,$tdef_Coq.Relations.Relation_Definitions.relation,$tdef_$_type_13667,$tdef_$_type_29014,$tdef_$_type_8935,$tdef_$_type_393,$tdef_$_type_27007,$tdef_$_type_373,$tdef_$_type_12251,$tdef_$_type_8377,$tdef_$_type_4976,$tdef_Coq.setoid_ring.Field_theory.linear,$tdef_$_type_23696,$tdef_$_type_20144,$tdef_Prop,$tdef_$_type_9046,$tdef_$_type_30078,$tdef_$_type_32357,$tdef_$_type_22874,$tdef_$_type_29571,$tdef_$_type_29833,$tdef_$_type_16640,$tdef_$_type_2469,$tdef_Coq.micromega.RingMicromega.Op2,$tdef_$_type_16754,$tdef_$_type_7997,$tdef_$_type_166313,$tdef_$_type_23504,$tdef_$_type_29472,$tdef_Coq.Init.Byte.byte,$tdef_$_type_29709,$tdef_Coq.Reals.Rfunctions.Z_spec,$tdef_$_type_5522,$tdef_$_type_31898,$tdef_$_type_307,$tdef_$_type_8847,$tdef_$_type_22701,$tdef_$_type_31952,$tdef_Coq.ZArith.Zpower.Zdiv_rest_proofs,$tdef_Coq.Strings.String.string,$tdef_$_type_3420,$tdef_$_type_16606,$tdef_$_type_18054,$tdef_$_type_13011,$tdef_$_type_32250,$tdef_$_type_26315,$tdef_$_type_31633,$tdef_$_type_18117,$tdef_$_type_18076,$tdef_$_type_12041,$tdef_$_type_13480,$tdef_$_type_20742,$tdef_$_type_12222,$tdef_$_type_7394,$tdef_$_type_13622,$tdef_$_type_31887,$tdef_$_type_13632,$tdef_Coq.micromega.RingMicromega.Op1,$tdef_Coq.Init.Datatypes.CompareSpecT,$tdef_Coq.Init.Specif.sigT,$tdef_$_type_1372,$tdef_$_type_14832,$tdef_$_type_26661,$tdef_$_type_22657,$tdef_$_type_12820,$tdef_$_type_5471,$tdef_$_type_10125,$tdef_$_type_8748,$tdef_$_type_166723,$tdef_$_type_159569,$tdef_$_type_27330,$tdef_Coq.setoid_ring.Field_theory.rsplit,$tdef_$_type_301,$tdef_$_type_141300,$tdef_Coq.micromega.EnvRing.Pol,$tdef_$_type_31893,$tdef_$_type_11847,$tdef_$_type_16,$tdef_$_type_13499,$tdef_$_type_31901,$tdef_$_type_32451,$tdef_$_type_31363,$tdef_$_type_154381,$tdef_$_type_29696,$tdef_$_type_102742,$tdef_$_type_99424,$tdef_$_type_29725,$tdef_$_type_15259,$tdef_$_type_364,$tdef_$_type_23691,$tdef_$_type_20841,$tdef_$_type_16818,$tdef_$_type_17620,$tdef_$_type_5384,$tdef_Coq.Structures.OrderedType.Compare,$tdef_Coq.Init.Specif.sumor,$tdef_$_type_31881,$tdef_$_type_16731,$tdef_$_type_22709,$tdef_$_type_166277,$tdef_$_type_322,$tdef_$_type_17946,$tdef_$_type_1390,$tdef_Coq.Structures.OrderedTypeEx.String_as_OT.t,$tdef_$_type_32239,$tdef_$_type_9034,$tdef_$_type_493,$tdef_$_type_13112,$tdef_$_type_4596,$tdef_$_type_438,$tdef_Coq.Bool.Bool.reflect,$tdef_$_type_29734,$tdef_$_type_22791,$tdef_$_type_29568,$tdef_Coq.setoid_ring.Ring_polynom.Pol,$tdef_$_type_31818,$tdef_$_type_355,$tdef_$_type_16800,$tdef_$_type_12066,$tdef_$_type_5921,$tdef_$_type_640,$tdef_$_type_836,$tdef_$_type_15262,$tdef_$_type_367,$tdef_$_type_99548,$tdef_$_type_2115,$tdef_Coq.Numbers.BinNums.Z,$tdef_$_type_5495,$tdef_$_type_8158,$tdef_$_type_29886,$tdef_$_type_29750,$tdef_$_type_17892,$tdef_Coq.QArith.QArith_base.Q,$tdef_$_type_166389,$tdef_$_type_24608,$tdef_Coq.Numbers.BinNums.positive,$tdef_$_type_2090,$tdef_Coq.Init.Datatypes.nat,$tdef_$_type_8976,$tdef_$_type_20269,$tdef_$_type_13314,$tdef_$_type_21039,$tdef_$_type_5300,$tdef_$_type_5438,$tdef_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$tdef_$_type_156168,$tdef_$_type_2514,$tdef_$_type_1197,$tdef_$_type_24262,$tdef_$_type_29739,$tdef_$_type_31374,$tdef_Coq.Init.Datatypes.prod,$tdef_$_type_18407,$tdef_$_type_103179,$tdef_Coq.micromega.RingMicromega.Formula,$tdef_$_type_1279,$tdef_$_type_10113,$tdef_$_type_17988,$tdef_Coq.setoid_ring.Ring_polynom.PExpr,$tdef_$_type_154397,$tdef_$_type_2404,$tdef_$_type_462,$tdef_$_type_20068,$tdef_$_type_10585,$tdef_$_type_4913,$tdef_$_type_18097,$tdef_$_type_12237,$tdef_$_type_20530,$tdef_Coq.setoid_ring.Ring_theory.ring_kind,$tdef_$_type_103177,$tdef_$_type_17245,$tdef_$_type_23614,$tdef_Coq.Vectors.VectorDef.t,$tdef_$_type_5030,$tdef_$_type_16777,$tdef_$_type_24954,$tdef_$_type_12109,$tdef_$_type_10055,$tdef_$_type_24,$tdef_$_type_1104,$tdef_Type,$tdef_Coq.PArith.BinPosDef.Pos.mask,$tdef_$_type_22693,$tdef_$_type_28022,$tdef_$_type_31241,$tdef_$_type_166386,$tdef_$_type_17495,$tdef_$_type_16844,$tdef_$_type_10047,$tdef_$_type_10574,$tdef_$_type_8840,$tdef_Coq.Vectors.Fin.t,$tdef_Coq.Reals.RIneq.nonzeroreal,$tdef_$_type_29957,$tdef_$_type_18034,$tdef_$_type_20574,$tdef_$_type_30714,$tdef_$_type_18023,$tdef_$_type_31798,$tdef_$_type_1381,$tdef_$_type_16603,$tdef_$_type_11910,$tdef_$_type_29893,$tdef_$_type_29747,$tdef_$_type_1022,$tdef_$_type_29362,$tdef_$_type_28668,$tdef_$_type_32472,$tdef_$_type_8595,$tdef_$_type_30661,$tdef_$_type_166299,$tdef_$_type_470,$tdef_$_type_16862,$tdef_$_type_166378] % 11.02/11.73 =============================================================== % 11.02/11.73 % 11.02/11.73 Combined formula: 2538 axiom(s) => conjecture % 11.02/11.73 % 11.02/11.73 % Equality/functions detected -> nanoCoP oracle mode % 11.02/11.73 nanoCoP : % 11.02/11.73 % 10,182,836 inferences, 8.449 CPU in 8.448 seconds (100% CPU, 1205240 Lips) % 11.02/11.73 % 11.02/11.73 % nanoCoP proof (equality/functions) % 11.02/11.73 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 11.02/11.73 % 11.02/11.73 % SZS output end Proof %------------------------------------------------------------------------------