%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SEV608+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 : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 12 07:13:47 PM UTC 2026 % Result : Theorem 23.70s 23.20s % Output : Proof 23.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.14 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.18/0.35 % Computer : n027.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Mon May 11 14:06:35 EDT 2026 % 0.18/0.35 % CPUTime : % 23.70/23.20 % SZS status Theorem % 23.70/23.20 % SZS output start Proof % 23.70/23.20 % 23.70/23.20 =============================================================== % 23.70/23.20 TPTP Problem: _HAMMER_GOAL (conjecture with 2867 axiom(s)) % 23.70/23.20 Axioms: [_HAMMER_COQ_TRUE,_HAMMER_COQ_FALSE,_HAMMER_COQ_TYPE_TYPE,$_case_Coq.Init.Datatypes.bool$186520,$_case_Coq.Init.Datatypes.bool$28461,$_case_Coq.Init.Datatypes.bool$39205,$_case_Coq.Init.Datatypes.prod$140898,$_case_Coq.Init.Datatypes.prod$147444,$_case_Coq.Init.Datatypes.prod$207653,$_case_Coq.Init.Specif.sumbool$28924,$_def_$_cast_193798,$_def_$_let_var_6_p_22552_22555,$_def_$_let_var_6_p_22554_22556,$_def_$_let_var_var_var_11_twoPQ_150915_150919_150922_150930,$_def_$_let_var_var_var_12_Q2_150916_150920_150923_150931,$_def_$_let_var_var_var_13_P2_150913_150918_150921_150932,$_def_$_let_var_var_var_var_var_14_QQ'_145105_145121_145136_145148_145152_145178,$_def_$_let_var_var_var_var_var_14_QQ'_3685_3701_3716_3728_3732_3758,$_def_$_let_var_var_var_var_var_var_15_QQ'_145099_145115_145130_145162_145167_145171_145187,$_def_$_let_var_var_var_var_var_var_15_QQ'_3679_3695_3710_3742_3747_3751_3767,$_def_$_let_var_var_var_var_var_var_16_PQ'_145098_145114_145129_145161_145166_145170_145188,$_def_$_let_var_var_var_var_var_var_16_PQ'_3678_3694_3709_3741_3746_3750_3768,$_def_$_let_var_var_var_var_var_var_17_QP'_145096_145113_145128_145160_145165_145169_145189,$_def_$_let_var_var_var_var_var_var_17_QP'_3676_3693_3708_3740_3745_3749_3769,$_def_$_let_var_var_var_var_var_var_18_PP'_145094_145111_145126_145158_145164_145168_145190,$_def_$_let_var_var_var_var_var_var_18_PP'_3674_3691_3706_3738_3744_3748_3770,$_def_Color.Mdomain,$_def_Color.WP.Add,$_def_Color.WP.Partition,$_def_Color.WP.transpose_neqkey,$_def_Color.adj,$_def_Color.graph,$_def_Color.low_deg,$_def_Color.no_selfloop,$_def_Color.node,$_def_Color.nodemap,$_def_Color.nodes,$_def_Color.nodeset,$_def_Color.remove_node,$_def_Color.select_F,$_def_Color.subset_nodes,$_def_Color.undirected,$_def_Coq.Arith.Between.in_int,$_def_Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.interp_ord,$_def_Coq.Arith.PeanoNat.Nat.Private_Tac.interp_ord,$_def_Coq.Arith.PeanoNat.Nat.b2n,$_def_Coq.Arith.PeanoNat.Nat.eqf,$_def_Coq.Arith.PeanoNat.Nat.lt,$_def_Coq.Arith.Wf_nat.ltof,$_def_Coq.Bool.Bool.eqb,$_def_Coq.FSets.FMapPositive.PositiveMap.Empty,$_def_Coq.FSets.FMapPositive.PositiveMap.Equal,$_def_Coq.FSets.FMapPositive.PositiveMap.In,$_def_Coq.FSets.FMapPositive.PositiveMap.MapsTo,$_def_Coq.FSets.FMapPositive.PositiveMap.add,$_def_Coq.FSets.FMapPositive.PositiveMap.cardinal,$_def_Coq.FSets.FMapPositive.PositiveMap.elements,$_def_Coq.FSets.FMapPositive.PositiveMap.eq_key_elt,$_def_Coq.FSets.FMapPositive.PositiveMap.find,$_def_Coq.FSets.FMapPositive.PositiveMap.fold,$_def_Coq.FSets.FMapPositive.PositiveMap.key,$_def_Coq.FSets.FMapPositive.PositiveMap.map,$_def_Coq.FSets.FMapPositive.PositiveMap.map2,$_def_Coq.FSets.FMapPositive.PositiveMap.mem,$_def_Coq.FSets.FMapPositive.PositiveMap.remove,$_def_Coq.FSets.FMapPositive.PositiveMap.t,$_def_Coq.FSets.FMapPositive.PositiveMap.xelements,$_def_Coq.FSets.FMapPositive.PositiveMap.xfind,$_def_Coq.FSets.FMapPositive.PositiveMap.xmap2_l,$_def_Coq.FSets.FMapPositive.PositiveMap.xmap2_r,$_def_Coq.FSets.FMapPositive.append,$_def_Coq.FSets.FSetPositive.PositiveSet.Empty,$_def_Coq.FSets.FSetPositive.PositiveSet.Equal,$_def_Coq.FSets.FSetPositive.PositiveSet.In,$_def_Coq.FSets.FSetPositive.PositiveSet.Subset,$_def_Coq.FSets.FSetPositive.PositiveSet.add,$_def_Coq.FSets.FSetPositive.PositiveSet.cardinal,$_def_Coq.FSets.FSetPositive.PositiveSet.choose,$_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.fold,$_def_Coq.FSets.FSetPositive.PositiveSet.inter,$_def_Coq.FSets.FSetPositive.PositiveSet.is_empty,$_def_Coq.FSets.FSetPositive.PositiveSet.max_elt,$_def_Coq.FSets.FSetPositive.PositiveSet.mem,$_def_Coq.FSets.FSetPositive.PositiveSet.min_elt,$_def_Coq.FSets.FSetPositive.PositiveSet.omap,$_def_Coq.FSets.FSetPositive.PositiveSet.remove,$_def_Coq.FSets.FSetPositive.PositiveSet.singleton,$_def_Coq.FSets.FSetPositive.PositiveSet.t,$_def_Coq.FSets.FSetPositive.PositiveSet.union,$_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.option_map,$_def_Coq.Init.Datatypes.option_rec,$_def_Coq.Init.Datatypes.option_rect,$_def_Coq.Init.Datatypes.orb,$_def_Coq.Init.Datatypes.snd,$_def_Coq.Init.Nat.add,$_def_Coq.Init.Nat.compare,$_def_Coq.Init.Nat.div,$_def_Coq.Init.Nat.div2,$_def_Coq.Init.Nat.leb,$_def_Coq.Init.Nat.log2_iter,$_def_Coq.Init.Nat.ltb,$_def_Coq.Init.Nat.max,$_def_Coq.Init.Nat.min,$_def_Coq.Init.Nat.mul,$_def_Coq.Init.Nat.pow,$_def_Coq.Init.Nat.pred,$_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.value,$_def_Coq.Init.Wf.well_founded,$_def_Coq.Lists.List.In,$_def_Coq.Lists.List.existsb,$_def_Coq.Lists.List.find,$_def_Coq.Lists.List.fold_left,$_def_Coq.Lists.List.fold_right,$_def_Coq.Lists.List.hd,$_def_Coq.Lists.List.hd_error,$_def_Coq.Lists.List.map,$_def_Coq.Lists.List.nth,$_def_Coq.Lists.List.nth_error,$_def_Coq.Lists.List.rev,$_def_Coq.Lists.List.tl,$_def_Coq.Lists.SetoidList.compat_op,$_def_Coq.Lists.SetoidList.findA,$_def_Coq.Lists.SetoidList.transpose,$_def_Coq.Logic.Decidable.decidable,$_def_Coq.Logic.FinFun.Injective,$_def_Coq.Logic.FinFun.bFun,$_def_Coq.Logic.FinFun.bInjective,$_def_Coq.Logic.FinFun.bSurjective,$_def_Coq.NArith.BinNat.N.lt,$_def_Coq.NArith.BinNatDef.N.add,$_def_Coq.NArith.BinNatDef.N.compare,$_def_Coq.NArith.BinNatDef.N.leb,$_def_Coq.NArith.BinNatDef.N.of_nat,$_def_Coq.NArith.BinNatDef.N.to_nat,$_def_Coq.PArith.BinPos.Pos.le,$_def_Coq.PArith.BinPos.Pos.lt,$_def_Coq.PArith.BinPosDef.Pos.add,$_def_Coq.PArith.BinPosDef.Pos.compare,$_def_Coq.PArith.BinPosDef.Pos.max,$_def_Coq.PArith.BinPosDef.Pos.mul,$_def_Coq.PArith.BinPosDef.Pos.pred_double,$_def_Coq.PArith.BinPosDef.Pos.succ,$_def_Coq.Reals.Rdefinitions.IZR,$_def_Coq.Relations.Relation_Definitions.relation,$_def_Coq.Strings.Ascii.N_of_ascii,$_def_Coq.Strings.Ascii.nat_of_ascii,$_def_Coq.Strings.Byte.to_N,$_def_Coq.Strings.Byte.to_nat,$_def_Coq.Strings.String.get,$_def_Coq.Strings.String.index,$_def_Coq.Strings.String.length,$_def_Coq.Strings.String.prefix,$_def_Coq.Strings.String.substring,$_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.lt,$_def_Coq.ZArith.BinInt.Z.divide,$_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.add,$_def_Coq.ZArith.BinIntDef.Z.compare,$_def_Coq.ZArith.BinIntDef.Z.div,$_def_Coq.ZArith.BinIntDef.Z.gcd,$_def_Coq.ZArith.BinIntDef.Z.gtb,$_def_Coq.ZArith.BinIntDef.Z.leb,$_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.pos_sub,$_def_Coq.ZArith.BinIntDef.Z.pow,$_def_Coq.ZArith.BinIntDef.Z.sub,$_def_Coq.ZArith.BinIntDef.Z.succ,$_def_Coq.ZArith.Zbool.Zeq_bool,$_def_Coq.micromega.Env.Env,$_def_Coq.micromega.EnvRing.MPcond,$_def_Coq.micromega.EnvRing.Mphi,$_def_Coq.micromega.EnvRing.P0,$_def_Coq.micromega.EnvRing.PNSubst,$_def_Coq.micromega.EnvRing.PNSubst1,$_def_Coq.micromega.EnvRing.POneSubst,$_def_Coq.micromega.EnvRing.PSubstL,$_def_Coq.micromega.EnvRing.PSubstL1,$_def_Coq.micromega.EnvRing.Padd,$_def_Coq.micromega.EnvRing.PaddC,$_def_Coq.micromega.EnvRing.PaddI,$_def_Coq.micromega.EnvRing.PaddX,$_def_Coq.micromega.EnvRing.Pmul,$_def_Coq.micromega.EnvRing.PmulC,$_def_Coq.micromega.EnvRing.PmulC_aux,$_def_Coq.micromega.EnvRing.PmulI,$_def_Coq.micromega.EnvRing.Pphi,$_def_Coq.micromega.EnvRing.Psquare,$_def_Coq.micromega.EnvRing.PsubC,$_def_Coq.micromega.EnvRing.mkPX,$_def_Coq.micromega.EnvRing.mkPinj,$_def_Coq.micromega.Refl.make_conj,$_def_Coq.micromega.Refl.make_impl,$_def_Coq.micromega.RingMicromega.NFormula,$_def_Coq.micromega.RingMicromega.OpAdd,$_def_Coq.micromega.RingMicromega.OpMult,$_def_Coq.micromega.RingMicromega.PolC,$_def_Coq.micromega.RingMicromega.PolEnv,$_def_Coq.micromega.RingMicromega.cltb,$_def_Coq.micromega.RingMicromega.eval_nformula,$_def_Coq.micromega.RingMicromega.eval_op1,$_def_Coq.micromega.RingMicromega.eval_pol,$_def_Coq.micromega.RingMicromega.extract_hyps,$_def_Coq.micromega.RingMicromega.map_option,$_def_Coq.micromega.RingMicromega.map_option2,$_def_Coq.micromega.RingMicromega.nformula_plus_nformula,$_def_Coq.micromega.RingMicromega.nformula_times_nformula,$_def_Coq.micromega.RingMicromega.nhyps_of_psatz,$_def_Coq.micromega.RingMicromega.padd,$_def_Coq.micromega.RingMicromega.pexpr_times_nformula,$_def_Coq.micromega.RingMicromega.psubC,$_def_Coq.micromega.Tauto.and_cnf,$_def_Coq.micromega.Tauto.clause,$_def_Coq.micromega.Tauto.cnf,$_def_Coq.micromega.Tauto.cnf_checker,$_def_Coq.micromega.Tauto.cnf_ff,$_def_Coq.micromega.Tauto.cnf_tt,$_def_Coq.micromega.Tauto.eval_clause,$_def_Coq.micromega.Tauto.eval_cnf,$_def_Coq.micromega.Tauto.eval_f,$_def_Coq.micromega.Tauto.eval_opt_clause,$_def_Coq.micromega.Tauto.eval_tt,$_def_Coq.micromega.Tauto.or_clause,$_def_Coq.micromega.ZMicromega.ZWitness,$_def_Coq.micromega.ZMicromega.Zdiv_pol,$_def_Coq.micromega.ZMicromega.Zgcd_pol,$_def_Coq.micromega.ZMicromega.ceiling,$_def_Coq.micromega.ZMicromega.eval_Psatz,$_def_Coq.micromega.ZMicromega.eval_nformula,$_def_Coq.micromega.ZMicromega.eval_pol,$_def_Coq.micromega.ZMicromega.makeCuttingPlane,$_def_Coq.micromega.ZMicromega.nformula_of_cutting_plane,$_def_Coq.micromega.ZMicromega.padd,$_def_Coq.setoid_ring.BinList.jump,$_def_Coq.setoid_ring.Ring_polynom.MPcond,$_def_Coq.setoid_ring.Ring_polynom.Mphi,$_def_Coq.setoid_ring.Ring_polynom.P0,$_def_Coq.setoid_ring.Ring_polynom.PEeval,$_def_Coq.setoid_ring.Ring_polynom.PNSubst,$_def_Coq.setoid_ring.Ring_polynom.PNSubst1,$_def_Coq.setoid_ring.Ring_polynom.POneSubst,$_def_Coq.setoid_ring.Ring_polynom.PSubstL,$_def_Coq.setoid_ring.Ring_polynom.PSubstL1,$_def_Coq.setoid_ring.Ring_polynom.Padd,$_def_Coq.setoid_ring.Ring_polynom.PaddC,$_def_Coq.setoid_ring.Ring_polynom.PaddI,$_def_Coq.setoid_ring.Ring_polynom.PaddX,$_def_Coq.setoid_ring.Ring_polynom.Peq,$_def_Coq.setoid_ring.Ring_polynom.Pequiv,$_def_Coq.setoid_ring.Ring_polynom.Pmul,$_def_Coq.setoid_ring.Ring_polynom.PmulC,$_def_Coq.setoid_ring.Ring_polynom.PmulC_aux,$_def_Coq.setoid_ring.Ring_polynom.PmulI,$_def_Coq.setoid_ring.Ring_polynom.Pphi,$_def_Coq.setoid_ring.Ring_polynom.mkPX,$_def_Coq.setoid_ring.Ring_polynom.mkPinj,$_def_Coq.setoid_ring.Ring_polynom.mkVmon,$_def_Coq.setoid_ring.Ring_polynom.mkZmon,$_def_Coq.setoid_ring.Ring_polynom.mon_of_pol,$_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.FMapPositive.PositiveMap.Leaf$Coq.FSets.FMapPositive.PositiveMap.Node,$_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.Decimal.Nil$Coq.Init.Decimal.D0,$_discrim_Coq.Init.Decimal.Pos$Coq.Init.Decimal.Neg,$_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.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.PsatzIn$Coq.micromega.RingMicromega.PsatzSquare,$_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,$_fix_2314_1_add_carry,$_inj_Coq.Bool.Bool.ReflectF,$_inj_Coq.Bool.Bool.ReflectT,$_inj_Coq.FSets.FMapPositive.PositiveMap.Leaf,$_inj_Coq.FSets.FMapPositive.PositiveMap.Node,$_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.Decimal.D0,$_inj_Coq.Init.Decimal.D1,$_inj_Coq.Init.Decimal.D2,$_inj_Coq.Init.Decimal.D3,$_inj_Coq.Init.Decimal.D4,$_inj_Coq.Init.Decimal.D5,$_inj_Coq.Init.Decimal.D6,$_inj_Coq.Init.Decimal.D7,$_inj_Coq.Init.Decimal.D8,$_inj_Coq.Init.Decimal.D9,$_inj_Coq.Init.Decimal.Neg,$_inj_Coq.Init.Decimal.Pos,$_inj_Coq.Init.Specif.exist,$_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.QArith.QArith_base.Qmake,$_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.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.RingMicromega.PsatzAdd,$_inj_Coq.micromega.RingMicromega.PsatzC,$_inj_Coq.micromega.RingMicromega.PsatzIn,$_inj_Coq.micromega.RingMicromega.PsatzMulC,$_inj_Coq.micromega.RingMicromega.PsatzMulE,$_inj_Coq.micromega.RingMicromega.PsatzSquare,$_inj_Coq.micromega.RingMicromega.PsatzZ,$_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,$_inversion_Coq.Bool.Bool.reflect,$_inversion_Coq.FSets.FMapPositive.PositiveMap.tree,$_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.Decimal.int,$_inversion_Coq.Init.Decimal.uint,$_inversion_Coq.Init.Peano.le,$_inversion_Coq.Init.Specif.sig,$_inversion_Coq.Init.Specif.sumbool,$_inversion_Coq.Init.Specif.sumor,$_inversion_Coq.Init.Wf.Acc,$_inversion_Coq.Lists.List.NoDup,$_inversion_Coq.Lists.SetoidList.InA,$_inversion_Coq.Lists.SetoidList.NoDupA,$_inversion_Coq.Numbers.BinNums.N,$_inversion_Coq.Numbers.BinNums.Z,$_inversion_Coq.Numbers.BinNums.positive,$_inversion_Coq.QArith.QArith_base.Q,$_inversion_Coq.Sorting.Permutation.Permutation,$_inversion_Coq.Strings.Ascii.ascii,$_inversion_Coq.Strings.String.string,$_inversion_Coq.Structures.OrderedType.Compare,$_inversion_Coq.Structures.OrdersTac.ord,$_inversion_Coq.Vectors.Fin.t,$_inversion_Coq.Vectors.VectorDef.t,$_inversion_Coq.ZArith.Znumtheory.Zis_gcd,$_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.Psatz,$_inversion_Coq.micromega.RingMicromega.SORaddon,$_inversion_Coq.micromega.Tauto.GFormula,$_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_morph,$_inversion_Coq.setoid_ring.Ring_theory.sign_theory,$_lam_150690,$_lam_150698,$_lam_150706,$_lam_150714,$_lam_152682,$_lam_152789,$_lam_194304,$_lam_206374,$_lam_206585,$_lam_209153,$_lam_2569,$_lam_26889,$_lam_41777,$_lam_41984,$_lam_60496,$_prop_143705,$_prop_187903,$_prop_187904,$_prop_187905,$_prop_187906,$_prop_26964,$_prop_26965,$_prop_28933,$_prop_28934,$_prop_28935,$_prop_28936,$_prop_29976,$_prop_40945,$_type_1006,$_type_1009,$_type_10129,$_type_10230,$_type_1033,$_type_10331,$_type_1039,$_type_1041,$_type_10421,$_type_1044,$_type_1046,$_type_1048,$_type_10522,$_type_1058,$_type_10623,$_type_1070,$_type_10724,$_type_11489,$_type_11645,$_type_11650,$_type_11656,$_type_11658,$_type_12,$_type_124,$_type_1334,$_type_1338,$_type_1344,$_type_134676,$_type_135002,$_type_135373,$_type_135379,$_type_135700,$_type_137465,$_type_137608,$_type_137619,$_type_140643,$_type_140693,$_type_140743,$_type_140785,$_type_140835,$_type_140911,$_type_141004,$_type_141018,$_type_141053,$_type_141079,$_type_141195,$_type_141336,$_type_141435,$_type_141529,$_type_141644,$_type_141875,$_type_143,$_type_143703,$_type_143734,$_type_144054,$_type_144561,$_type_144633,$_type_144641,$_type_144757,$_type_144962,$_type_145067,$_type_145246,$_type_145866,$_type_145995,$_type_146123,$_type_146242,$_type_146385,$_type_146557,$_type_147700,$_type_149266,$_type_149503,$_type_149532,$_type_149684,$_type_149784,$_type_149808,$_type_150420,$_type_150446,$_type_150673,$_type_150757,$_type_150800,$_type_150809,$_type_150981,$_type_1511,$_type_1522,$_type_152508,$_type_152513,$_type_152516,$_type_152615,$_type_152738,$_type_152817,$_type_153862,$_type_153912,$_type_154688,$_type_155027,$_type_155137,$_type_155161,$_type_155307,$_type_163,$_type_168,$_type_1771,$_type_1779,$_type_18960,$_type_18965,$_type_18973,$_type_18976,$_type_19049,$_type_19055,$_type_193265,$_type_193283,$_type_193292,$_type_19352,$_type_193771,$_type_193820,$_type_19425,$_type_19454,$_type_19458,$_type_194701,$_type_194742,$_type_19706,$_type_197185,$_type_1995,$_type_2004,$_type_2012,$_type_206562,$_type_206565,$_type_206568,$_type_206573,$_type_206587,$_type_206591,$_type_206598,$_type_206605,$_type_206714,$_type_206780,$_type_206782,$_type_206793,$_type_206808,$_type_206811,$_type_206816,$_type_206819,$_type_206943,$_type_207018,$_type_207068,$_type_208002,$_type_208147,$_type_208170,$_type_208937,$_type_208948,$_type_208957,$_type_208986,$_type_209029,$_type_209098,$_type_209214,$_type_2219,$_type_22566,$_type_22587,$_type_2265,$_type_2274,$_type_2277,$_type_22841,$_type_22904,$_type_22967,$_type_2301,$_type_23021,$_type_23084,$_type_2344,$_type_2373,$_type_23752,$_type_23782,$_type_23806,$_type_23836,$_type_23866,$_type_23890,$_type_2390,$_type_23923,$_type_23947,$_type_23974,$_type_24427,$_type_24640,$_type_24853,$_type_25048,$_type_25261,$_type_25474,$_type_2567,$_type_25687,$_type_25900,$_type_26095,$_type_26308,$_type_26503,$_type_26608,$_type_26627,$_type_2663,$_type_26641,$_type_2672,$_type_26828,$_type_26851,$_type_26856,$_type_26868,$_type_26959,$_type_26962,$_type_27043,$_type_27051,$_type_27077,$_type_27113,$_type_27144,$_type_27353,$_type_27361,$_type_27366,$_type_27417,$_type_2742,$_type_27428,$_type_27433,$_type_27516,$_type_27563,$_type_28348,$_type_28399,$_type_28467,$_type_28478,$_type_28483,$_type_28492,$_type_29146,$_type_29153,$_type_29167,$_type_29181,$_type_29285,$_type_29310,$_type_29345,$_type_29352,$_type_29379,$_type_29392,$_type_30051,$_type_30735,$_type_30779,$_type_30815,$_type_30859,$_type_30881,$_type_30905,$_type_30909,$_type_30974,$_type_3102,$_type_31409,$_type_31619,$_type_31648,$_type_31653,$_type_31657,$_type_31669,$_type_31673,$_type_31712,$_type_31939,$_type_31946,$_type_31970,$_type_31977,$_type_32021,$_type_32037,$_type_32039,$_type_32042,$_type_32678,$_type_33024,$_type_3304,$_type_3307,$_type_33370,$_type_33693,$_type_3370,$_type_34039,$_type_34385,$_type_34731,$_type_3489,$_type_35077,$_type_3540,$_type_35423,$_type_35746,$_type_36092,$_type_36438,$_type_3645,$_type_3656,$_type_36761,$_type_37084,$_type_37430,$_type_37450,$_type_37454,$_type_378,$_type_3826,$_type_38767,$_type_38777,$_type_38791,$_type_38819,$_type_38837,$_type_38854,$_type_38871,$_type_38898,$_type_38950,$_type_39078,$_type_39104,$_type_39208,$_type_39577,$_type_4026,$_type_4031,$_type_40333,$_type_4040,$_type_40740,$_type_41152,$_type_41266,$_type_41347,$_type_41774,$_type_41945,$_type_41968,$_type_41971,$_type_41993,$_type_42004,$_type_42262,$_type_42313,$_type_4236,$_type_42451,$_type_43087,$_type_4329,$_type_43295,$_type_4422,$_type_44845,$_type_4504,$_type_4597,$_type_4679,$_type_471,$_type_47282,$_type_47286,$_type_47339,$_type_47342,$_type_47431,$_type_4772,$_type_49,$_type_494,$_type_506,$_type_518,$_type_520,$_type_530,$_type_53755,$_type_53787,$_type_54250,$_type_54379,$_type_54401,$_type_54616,$_type_550,$_type_55311,$_type_56096,$_type_56111,$_type_56314,$_type_56929,$_type_570,$_type_57076,$_type_576,$_type_59359,$_type_595,$_type_597,$_type_60498,$_type_60622,$_type_60798,$_type_60800,$_type_624,$_type_632,$_type_656,$_type_678,$_type_681,$_type_683,$_type_702,$_type_710,$_type_725,$_type_738,$_type_750,$_type_761,$_type_802,$_type_8057,$_type_8071,$_type_8078,$_type_907,$_type_9662,$_type_9671,$_type_9685,$_type_9692,$_typeof_Color.Mdomain,$_typeof_Color.WP.Add,$_typeof_Color.WP.Partition,$_typeof_Color.WP.fold_rel,$_typeof_Color.WP.transpose_neqkey,$_typeof_Color.adj,$_typeof_Color.graph,$_typeof_Color.low_deg,$_typeof_Color.no_selfloop,$_typeof_Color.node,$_typeof_Color.nodemap,$_typeof_Color.nodes,$_typeof_Color.nodeset,$_typeof_Color.remove_node,$_typeof_Color.select_F,$_typeof_Color.subset_nodes,$_typeof_Color.undirected,$_typeof_Coq.Arith.Between.in_int,$_typeof_Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.interp_ord,$_typeof_Coq.Arith.PeanoNat.Nat.Private_Tac.interp_ord,$_typeof_Coq.Arith.PeanoNat.Nat.b2n,$_typeof_Coq.Arith.PeanoNat.Nat.eqf,$_typeof_Coq.Arith.PeanoNat.Nat.lt,$_typeof_Coq.Arith.Wf_nat.ltof,$_typeof_Coq.Bool.Bool.eqb,$_typeof_Coq.Bool.Bool.reflect,$_typeof_Coq.FSets.FMapPositive.PositiveMap.Empty,$_typeof_Coq.FSets.FMapPositive.PositiveMap.Equal,$_typeof_Coq.FSets.FMapPositive.PositiveMap.In,$_typeof_Coq.FSets.FMapPositive.PositiveMap.Leaf,$_typeof_Coq.FSets.FMapPositive.PositiveMap.MapsTo,$_typeof_Coq.FSets.FMapPositive.PositiveMap.Node,$_typeof_Coq.FSets.FMapPositive.PositiveMap.add,$_typeof_Coq.FSets.FMapPositive.PositiveMap.cardinal,$_typeof_Coq.FSets.FMapPositive.PositiveMap.elements,$_typeof_Coq.FSets.FMapPositive.PositiveMap.eq_key_elt,$_typeof_Coq.FSets.FMapPositive.PositiveMap.find,$_typeof_Coq.FSets.FMapPositive.PositiveMap.fold,$_typeof_Coq.FSets.FMapPositive.PositiveMap.key,$_typeof_Coq.FSets.FMapPositive.PositiveMap.map,$_typeof_Coq.FSets.FMapPositive.PositiveMap.map2,$_typeof_Coq.FSets.FMapPositive.PositiveMap.mem,$_typeof_Coq.FSets.FMapPositive.PositiveMap.remove,$_typeof_Coq.FSets.FMapPositive.PositiveMap.t,$_typeof_Coq.FSets.FMapPositive.PositiveMap.tree,$_typeof_Coq.FSets.FMapPositive.PositiveMap.xelements,$_typeof_Coq.FSets.FMapPositive.PositiveMap.xfind,$_typeof_Coq.FSets.FMapPositive.PositiveMap.xmap2_l,$_typeof_Coq.FSets.FMapPositive.PositiveMap.xmap2_r,$_typeof_Coq.FSets.FMapPositive.append,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Equal,$_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.add,$_typeof_Coq.FSets.FSetPositive.PositiveSet.cardinal,$_typeof_Coq.FSets.FSetPositive.PositiveSet.choose,$_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.fold,$_typeof_Coq.FSets.FSetPositive.PositiveSet.inter,$_typeof_Coq.FSets.FSetPositive.PositiveSet.is_empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.max_elt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.mem,$_typeof_Coq.FSets.FSetPositive.PositiveSet.min_elt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.omap,$_typeof_Coq.FSets.FSetPositive.PositiveSet.remove,$_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.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.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.inl,$_typeof_Coq.Init.Datatypes.inr,$_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.option_map,$_typeof_Coq.Init.Datatypes.option_rec,$_typeof_Coq.Init.Datatypes.option_rect,$_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.Decimal.int,$_typeof_Coq.Init.Decimal.uint,$_typeof_Coq.Init.Nat.add,$_typeof_Coq.Init.Nat.compare,$_typeof_Coq.Init.Nat.div,$_typeof_Coq.Init.Nat.div2,$_typeof_Coq.Init.Nat.leb,$_typeof_Coq.Init.Nat.log2_iter,$_typeof_Coq.Init.Nat.ltb,$_typeof_Coq.Init.Nat.max,$_typeof_Coq.Init.Nat.min,$_typeof_Coq.Init.Nat.mul,$_typeof_Coq.Init.Nat.pow,$_typeof_Coq.Init.Nat.pred,$_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.left,$_typeof_Coq.Init.Specif.proj1_sig,$_typeof_Coq.Init.Specif.right,$_typeof_Coq.Init.Specif.sig,$_typeof_Coq.Init.Specif.sumbool,$_typeof_Coq.Init.Specif.sumor,$_typeof_Coq.Init.Specif.value,$_typeof_Coq.Init.Wf.well_founded,$_typeof_Coq.Lists.List.In,$_typeof_Coq.Lists.List.existsb,$_typeof_Coq.Lists.List.find,$_typeof_Coq.Lists.List.fold_left,$_typeof_Coq.Lists.List.fold_right,$_typeof_Coq.Lists.List.hd,$_typeof_Coq.Lists.List.hd_error,$_typeof_Coq.Lists.List.map,$_typeof_Coq.Lists.List.nth,$_typeof_Coq.Lists.List.nth_error,$_typeof_Coq.Lists.List.nth_in_or_default,$_typeof_Coq.Lists.List.rev,$_typeof_Coq.Lists.List.tl,$_typeof_Coq.Lists.SetoidList.compat_op,$_typeof_Coq.Lists.SetoidList.findA,$_typeof_Coq.Lists.SetoidList.transpose,$_typeof_Coq.Logic.Decidable.decidable,$_typeof_Coq.Logic.FinFun.Injective,$_typeof_Coq.Logic.FinFun.bFun,$_typeof_Coq.Logic.FinFun.bInjective,$_typeof_Coq.Logic.FinFun.bSurjective,$_typeof_Coq.NArith.BinNat.N.lt,$_typeof_Coq.NArith.BinNatDef.N.add,$_typeof_Coq.NArith.BinNatDef.N.compare,$_typeof_Coq.NArith.BinNatDef.N.leb,$_typeof_Coq.NArith.BinNatDef.N.of_nat,$_typeof_Coq.NArith.BinNatDef.N.to_nat,$_typeof_Coq.Numbers.BinNums.N,$_typeof_Coq.Numbers.BinNums.N0,$_typeof_Coq.Numbers.BinNums.Npos,$_typeof_Coq.Numbers.BinNums.Z,$_typeof_Coq.Numbers.BinNums.Z0,$_typeof_Coq.Numbers.BinNums.Zneg,$_typeof_Coq.Numbers.BinNums.Zpos,$_typeof_Coq.Numbers.BinNums.positive,$_typeof_Coq.Numbers.BinNums.xH,$_typeof_Coq.Numbers.BinNums.xI,$_typeof_Coq.Numbers.BinNums.xO,$_typeof_Coq.PArith.BinPos.Pos.le,$_typeof_Coq.PArith.BinPos.Pos.lt,$_typeof_Coq.PArith.BinPosDef.Pos.add,$_typeof_Coq.PArith.BinPosDef.Pos.compare,$_typeof_Coq.PArith.BinPosDef.Pos.max,$_typeof_Coq.PArith.BinPosDef.Pos.mul,$_typeof_Coq.PArith.BinPosDef.Pos.pred_double,$_typeof_Coq.PArith.BinPosDef.Pos.succ,$_typeof_Coq.QArith.QArith_base.Q,$_typeof_Coq.Reals.Rdefinitions.IZR,$_typeof_Coq.Reals.Rdefinitions.R,$_typeof_Coq.Reals.Rdefinitions.Rlt,$_typeof_Coq.Reals.Rdefinitions.Rplus,$_typeof_Coq.Relations.Relation_Definitions.relation,$_typeof_Coq.Strings.Ascii.N_of_ascii,$_typeof_Coq.Strings.Ascii.ascii,$_typeof_Coq.Strings.Ascii.nat_of_ascii,$_typeof_Coq.Strings.Byte.to_N,$_typeof_Coq.Strings.Byte.to_nat,$_typeof_Coq.Strings.String.EmptyString,$_typeof_Coq.Strings.String.String,$_typeof_Coq.Strings.String.get,$_typeof_Coq.Strings.String.index,$_typeof_Coq.Strings.String.length,$_typeof_Coq.Strings.String.prefix,$_typeof_Coq.Strings.String.string,$_typeof_Coq.Strings.String.substring,$_typeof_Coq.Structures.OrderedType.Compare,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_dec,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.lt,$_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.t,$_typeof_Coq.ZArith.BinInt.Z.divide,$_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.add,$_typeof_Coq.ZArith.BinIntDef.Z.compare,$_typeof_Coq.ZArith.BinIntDef.Z.div,$_typeof_Coq.ZArith.BinIntDef.Z.gcd,$_typeof_Coq.ZArith.BinIntDef.Z.gtb,$_typeof_Coq.ZArith.BinIntDef.Z.leb,$_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.pos_sub,$_typeof_Coq.ZArith.BinIntDef.Z.pow,$_typeof_Coq.ZArith.BinIntDef.Z.sub,$_typeof_Coq.ZArith.BinIntDef.Z.succ,$_typeof_Coq.ZArith.Zbool.Zeq_bool,$_typeof_Coq.micromega.Env.Env,$_typeof_Coq.micromega.EnvRing.MPcond,$_typeof_Coq.micromega.EnvRing.Mon,$_typeof_Coq.micromega.EnvRing.Mphi,$_typeof_Coq.micromega.EnvRing.P0,$_typeof_Coq.micromega.EnvRing.PExpr,$_typeof_Coq.micromega.EnvRing.PNSubst,$_typeof_Coq.micromega.EnvRing.PNSubst1,$_typeof_Coq.micromega.EnvRing.POneSubst,$_typeof_Coq.micromega.EnvRing.PSubstL,$_typeof_Coq.micromega.EnvRing.PSubstL1,$_typeof_Coq.micromega.EnvRing.PX,$_typeof_Coq.micromega.EnvRing.Padd,$_typeof_Coq.micromega.EnvRing.PaddC,$_typeof_Coq.micromega.EnvRing.PaddI,$_typeof_Coq.micromega.EnvRing.PaddX,$_typeof_Coq.micromega.EnvRing.Pc,$_typeof_Coq.micromega.EnvRing.Pinj,$_typeof_Coq.micromega.EnvRing.Pmul,$_typeof_Coq.micromega.EnvRing.PmulC,$_typeof_Coq.micromega.EnvRing.PmulC_aux,$_typeof_Coq.micromega.EnvRing.PmulI,$_typeof_Coq.micromega.EnvRing.Pol,$_typeof_Coq.micromega.EnvRing.Pphi,$_typeof_Coq.micromega.EnvRing.Psquare,$_typeof_Coq.micromega.EnvRing.PsubC,$_typeof_Coq.micromega.EnvRing.mkPX,$_typeof_Coq.micromega.EnvRing.mkPinj,$_typeof_Coq.micromega.Refl.make_conj,$_typeof_Coq.micromega.Refl.make_impl,$_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.OpAdd,$_typeof_Coq.micromega.RingMicromega.OpMult,$_typeof_Coq.micromega.RingMicromega.PolC,$_typeof_Coq.micromega.RingMicromega.PolEnv,$_typeof_Coq.micromega.RingMicromega.Psatz,$_typeof_Coq.micromega.RingMicromega.PsatzAdd,$_typeof_Coq.micromega.RingMicromega.PsatzC,$_typeof_Coq.micromega.RingMicromega.PsatzIn,$_typeof_Coq.micromega.RingMicromega.PsatzMulC,$_typeof_Coq.micromega.RingMicromega.PsatzMulE,$_typeof_Coq.micromega.RingMicromega.PsatzSquare,$_typeof_Coq.micromega.RingMicromega.PsatzZ,$_typeof_Coq.micromega.RingMicromega.Strict,$_typeof_Coq.micromega.RingMicromega.cltb,$_typeof_Coq.micromega.RingMicromega.eval_nformula,$_typeof_Coq.micromega.RingMicromega.eval_op1,$_typeof_Coq.micromega.RingMicromega.eval_pol,$_typeof_Coq.micromega.RingMicromega.extract_hyps,$_typeof_Coq.micromega.RingMicromega.map_option,$_typeof_Coq.micromega.RingMicromega.map_option2,$_typeof_Coq.micromega.RingMicromega.nformula_plus_nformula,$_typeof_Coq.micromega.RingMicromega.nformula_times_nformula,$_typeof_Coq.micromega.RingMicromega.nhyps_of_psatz,$_typeof_Coq.micromega.RingMicromega.padd,$_typeof_Coq.micromega.RingMicromega.pexpr_times_nformula,$_typeof_Coq.micromega.RingMicromega.psubC,$_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.and_cnf,$_typeof_Coq.micromega.Tauto.clause,$_typeof_Coq.micromega.Tauto.cnf,$_typeof_Coq.micromega.Tauto.cnf_checker,$_typeof_Coq.micromega.Tauto.cnf_ff,$_typeof_Coq.micromega.Tauto.cnf_tt,$_typeof_Coq.micromega.Tauto.eval_clause,$_typeof_Coq.micromega.Tauto.eval_cnf,$_typeof_Coq.micromega.Tauto.eval_f,$_typeof_Coq.micromega.Tauto.eval_opt_clause,$_typeof_Coq.micromega.Tauto.eval_tt,$_typeof_Coq.micromega.Tauto.or_clause,$_typeof_Coq.micromega.ZMicromega.Vars.Facts.choose_mem_3,$_typeof_Coq.micromega.ZMicromega.ZWitness,$_typeof_Coq.micromega.ZMicromega.Zdiv_pol,$_typeof_Coq.micromega.ZMicromega.Zgcd_pol,$_typeof_Coq.micromega.ZMicromega.ceiling,$_typeof_Coq.micromega.ZMicromega.eval_Psatz,$_typeof_Coq.micromega.ZMicromega.eval_nformula,$_typeof_Coq.micromega.ZMicromega.eval_pol,$_typeof_Coq.micromega.ZMicromega.makeCuttingPlane,$_typeof_Coq.micromega.ZMicromega.nformula_of_cutting_plane,$_typeof_Coq.micromega.ZMicromega.padd,$_typeof_Coq.setoid_ring.BinList.jump,$_typeof_Coq.setoid_ring.Field_theory.FExpr,$_typeof_Coq.setoid_ring.Field_theory.linear,$_typeof_Coq.setoid_ring.Field_theory.rsplit,$_typeof_Coq.setoid_ring.Ring_polynom.MPcond,$_typeof_Coq.setoid_ring.Ring_polynom.Mon,$_typeof_Coq.setoid_ring.Ring_polynom.Mphi,$_typeof_Coq.setoid_ring.Ring_polynom.P0,$_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.PExpr,$_typeof_Coq.setoid_ring.Ring_polynom.PNSubst,$_typeof_Coq.setoid_ring.Ring_polynom.PNSubst1,$_typeof_Coq.setoid_ring.Ring_polynom.POneSubst,$_typeof_Coq.setoid_ring.Ring_polynom.PSubstL,$_typeof_Coq.setoid_ring.Ring_polynom.PSubstL1,$_typeof_Coq.setoid_ring.Ring_polynom.PX,$_typeof_Coq.setoid_ring.Ring_polynom.Padd,$_typeof_Coq.setoid_ring.Ring_polynom.PaddC,$_typeof_Coq.setoid_ring.Ring_polynom.PaddI,$_typeof_Coq.setoid_ring.Ring_polynom.PaddX,$_typeof_Coq.setoid_ring.Ring_polynom.Pc,$_typeof_Coq.setoid_ring.Ring_polynom.Peq,$_typeof_Coq.setoid_ring.Ring_polynom.Pequiv,$_typeof_Coq.setoid_ring.Ring_polynom.Pinj,$_typeof_Coq.setoid_ring.Ring_polynom.Pmul,$_typeof_Coq.setoid_ring.Ring_polynom.PmulC,$_typeof_Coq.setoid_ring.Ring_polynom.PmulC_aux,$_typeof_Coq.setoid_ring.Ring_polynom.PmulI,$_typeof_Coq.setoid_ring.Ring_polynom.Pol,$_typeof_Coq.setoid_ring.Ring_polynom.Pphi,$_typeof_Coq.setoid_ring.Ring_polynom.mkPX,$_typeof_Coq.setoid_ring.Ring_polynom.mkPinj,$_typeof_Coq.setoid_ring.Ring_polynom.mkVmon,$_typeof_Coq.setoid_ring.Ring_polynom.mkZmon,$_typeof_Coq.setoid_ring.Ring_polynom.mon0,$_typeof_Coq.setoid_ring.Ring_polynom.mon_of_pol,$_typeof_Coq.setoid_ring.Ring_polynom.zmon,$_typeof_Coq.setoid_ring.Ring_theory.pow_N,$_typeof_Coq.setoid_ring.Ring_theory.pow_pos,Color.Mremove_cardinal_less,Color.WF.add_eq_o,Color.WF.eq_option_alt,Color.WF.find_mapsto_iff,Color.WF.map2_1bis,Color.WP.Equal_cardinal,Color.WP.F.add_eq_o,Color.WP.F.add_o,Color.WP.F.eq_option_alt,Color.WP.F.find_mapsto_iff,Color.WP.F.map2_1bis,Color.WP.Partition_cardinal,Color.WP.cardinal_1,Color.WP.cardinal_2,Color.WP.cardinal_Empty,Color.WP.cardinal_fold,Color.WP.cardinal_inv_1,Color.WP.cardinal_m,Color.WP.cardinal_m_Proper,Color.WP.fold_Equal,Color.cardinal_map,Color.select_terminates,Color.subset_nodes_sub,Coq.Arith.Compare_dec.not_eq,Coq.Arith.Gt.gt_S_le,Coq.Arith.Gt.gt_le_S,Coq.Arith.Le.le_S_n,Coq.Arith.Le.le_n_S,Coq.Arith.Lt.S_pred,Coq.Arith.Lt.le_lt_n_Sm,Coq.Arith.Lt.le_lt_or_eq,Coq.Arith.Lt.le_not_lt,Coq.Arith.Lt.lt_S_n,Coq.Arith.Lt.lt_le_S,Coq.Arith.Lt.lt_n_S,Coq.Arith.Lt.lt_not_le,Coq.Arith.Lt.nat_total_order,Coq.Arith.Lt.neq_0_lt,Coq.Arith.Minus.minus_Sn_m,Coq.Arith.PeanoNat.Nat.A'A_right,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.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.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_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.not_ge_lt,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_lt_mono,Coq.Arith.PeanoNat.Nat.add_lt_mono_l,Coq.Arith.PeanoNat.Nat.add_lt_mono_r,Coq.Arith.PeanoNat.Nat.add_wd,Coq.Arith.PeanoNat.Nat.compare_lt_iff,Coq.Arith.PeanoNat.Nat.eq_0_gt_0_cases,Coq.Arith.PeanoNat.Nat.eq_equiv,Coq.Arith.PeanoNat.Nat.eq_le_incl,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_lt_trans,Coq.Arith.PeanoNat.Nat.le_lteq,Coq.Arith.PeanoNat.Nat.le_ngt,Coq.Arith.PeanoNat.Nat.le_succ_l,Coq.Arith.PeanoNat.Nat.le_trans,Coq.Arith.PeanoNat.Nat.le_wd,Coq.Arith.PeanoNat.Nat.leb_le,Coq.Arith.PeanoNat.Nat.log2_lt_cancel,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_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_stepl,Coq.Arith.PeanoNat.Nat.lt_stepr,Coq.Arith.PeanoNat.Nat.lt_succ_diag_r,Coq.Arith.PeanoNat.Nat.lt_succ_l,Coq.Arith.PeanoNat.Nat.lt_succ_r,Coq.Arith.PeanoNat.Nat.lt_total,Coq.Arith.PeanoNat.Nat.lt_trans,Coq.Arith.PeanoNat.Nat.lt_trichotomy,Coq.Arith.PeanoNat.Nat.lt_wd,Coq.Arith.PeanoNat.Nat.max_spec,Coq.Arith.PeanoNat.Nat.min_spec,Coq.Arith.PeanoNat.Nat.mod_upper_bound,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_comm,Coq.Arith.PeanoNat.Nat.mul_lt_mono_pos_l,Coq.Arith.PeanoNat.Nat.mul_wd,Coq.Arith.PeanoNat.Nat.neq_0_lt_0,Coq.Arith.PeanoNat.Nat.neq_sym,Coq.Arith.PeanoNat.Nat.nlt_0_r,Coq.Arith.PeanoNat.Nat.nlt_ge,Coq.Arith.PeanoNat.Nat.one_succ,Coq.Arith.PeanoNat.Nat.succ_inj,Coq.Arith.PeanoNat.Nat.succ_lt_mono,Coq.Arith.PeanoNat.Nat.succ_wd,Coq.Arith.PeanoNat.Nat.two_succ,Coq.Arith.Peano_dec.dec_eq_nat,Coq.Arith.Plus.plus_lt_le_compat,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.eqb_true_iff,Coq.Bool.Bool.negb_false_iff,Coq.Bool.Bool.negb_true_iff,Coq.FSets.FMapPositive.PositiveMap.add_1,Coq.FSets.FMapPositive.PositiveMap.cardinal_1,Coq.FSets.FMapPositive.PositiveMap.elements_correct,Coq.FSets.FMapPositive.PositiveMap.find_1,Coq.FSets.FMapPositive.PositiveMap.find_2,Coq.FSets.FMapPositive.PositiveMap.find_xfind_h,Coq.FSets.FMapPositive.PositiveMap.gleaf,Coq.FSets.FMapPositive.PositiveMap.gmap2,Coq.FSets.FMapPositive.PositiveMap.gso,Coq.FSets.FMapPositive.PositiveMap.gss,Coq.FSets.FMapPositive.PositiveMap.map2_2,Coq.FSets.FMapPositive.PositiveMap.tree_ind,Coq.FSets.FMapPositive.PositiveMap.xelements_correct,Coq.FSets.FMapPositive.PositiveMap.xfind_left,Coq.FSets.FMapPositive.PositiveMap.xgmap2_l,Coq.FSets.FMapPositive.PositiveMap.xgmap2_r,Coq.FSets.FMapPositive.PositiveMapAdditionalFacts.gsident,Coq.FSets.FMapPositive.PositiveMapAdditionalFacts.map2_commut,Coq.FSets.FMapPositive.PositiveMapAdditionalFacts.xmap2_lr,Coq.FSets.FMapPositive.append_assoc_0,Coq.FSets.FMapPositive.append_assoc_1,Coq.FSets.FMapPositive.append_neutral_r,Coq.FSets.FSetPositive.PositiveSet.choose_1,Coq.FSets.FSetPositive.PositiveSet.choose_2,Coq.FSets.FSetPositive.PositiveSet.choose_3,Coq.FSets.FSetPositive.PositiveSet.choose_3',Coq.FSets.FSetPositive.PositiveSet.choose_empty,Coq.FSets.FSetPositive.PositiveSet.empty_1,Coq.FSets.FSetPositive.PositiveSet.eq_sym,Coq.FSets.FSetPositive.PositiveSet.equal_spec,Coq.FSets.FSetPositive.PositiveSet.is_empty_1,Coq.FSets.FSetPositive.PositiveSet.is_empty_2,Coq.FSets.FSetPositive.PositiveSet.max_elt_1,Coq.FSets.FSetPositive.PositiveSet.max_elt_2,Coq.FSets.FSetPositive.PositiveSet.max_elt_3,Coq.FSets.FSetPositive.PositiveSet.mem_1,Coq.FSets.FSetPositive.PositiveSet.min_elt_1,Coq.FSets.FSetPositive.PositiveSet.min_elt_2,Coq.FSets.FSetPositive.PositiveSet.min_elt_3,Coq.FSets.FSetPositive.PositiveSet.tree_ind,Coq.Init.Datatypes.andb_prop,Coq.Init.Datatypes.list_ind,Coq.Init.Datatypes.nat_ind,Coq.Init.Datatypes.option_ind,Coq.Init.Datatypes.option_sind,Coq.Init.Datatypes.prod_ind,Coq.Init.Peano.eq_add_S,Coq.Init.Peano.f_equal_nat,Coq.Init.Peano.le_S,Coq.Init.Peano.le_n,Coq.Init.Peano.plus_n_Sm,Coq.Lists.List.In_nth_error,Coq.Lists.List.NoDup_cons,Coq.Lists.List.NoDup_ind,Coq.Lists.List.NoDup_nil,Coq.Lists.List.NoDup_nth_error,Coq.Lists.List.app_length,Coq.Lists.List.find_none,Coq.Lists.List.find_some,Coq.Lists.List.fold_left_length,Coq.Lists.List.hd_error_cons,Coq.Lists.List.hd_error_some_nil,Coq.Lists.List.hd_error_tl_repr,Coq.Lists.List.in_app_or,Coq.Lists.List.in_cons,Coq.Lists.List.in_eq,Coq.Lists.List.in_inv,Coq.Lists.List.in_or_app,Coq.Lists.List.map_nth_error,Coq.Lists.List.nth_error_In,Coq.Lists.List.nth_error_Some,Coq.Lists.List.nth_error_split,Coq.Lists.SetoidList.InA_cons_hd,Coq.Lists.SetoidList.InA_cons_tl,Coq.Logic.Decidable.dec_not_not,Coq.NArith.Nnat.Nat2N.id,Coq.Numbers.BinNums.positive_ind,Coq.Setoids.Setoid.Seq_refl,Coq.Strings.Byte.of_to_N,Coq.Strings.Byte.of_to_nat,Coq.Strings.Byte.to_of_N,Coq.Strings.Byte.to_of_N_iff,Coq.Strings.Byte.to_of_nat,Coq.Strings.Byte.to_of_nat_iff,Coq.Strings.String.index_correct1,Coq.Strings.String.index_correct2,Coq.Strings.String.index_correct4,Coq.Strings.String.prefix_correct,Coq.Strings.String.string_ind,Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_refl,Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_sym,Coq.ZArith.BinInt.Z.add_0_r,Coq.ZArith.BinInt.Z.div_unique_exact,Coq.ZArith.BinInt.Z.divide_refl,Coq.ZArith.BinInt.Z.eq_decidable,Coq.ZArith.BinInt.Z.le_decidable,Coq.ZArith.BinInt.Z.lt_decidable,Coq.ZArith.BinInt.Z.mul_comm,Coq.ZArith.BinInt.Z.mul_eq_0,Coq.ZArith.BinInt.Z.mul_opp_l,Coq.ZArith.BinInt.Z.sub_move_0_r,Coq.ZArith.Zbool.Zeq_bool_eq,Coq.ZArith.Zbool.Zeq_bool_neq,Coq.ZArith.Zbool.Zgt_is_gt_bool,Coq.ZArith.Znat.Nat2Z.inj_add,Coq.ZArith.Znat.Nat2Z.inj_succ,Coq.ZArith.Znat.inj_neq,Coq.ZArith.Znumtheory.Zdivide_opp_r,Coq.ZArith.Znumtheory.Zgcd_is_gcd,Coq.ZArith.Znumtheory.Zis_gcd_intro,Coq.ZArith.Zorder.Znot_le_gt,Coq.ZArith.Zorder.Znot_lt_ge,Coq.ZArith.auxiliary.Zegal_left,Coq.ZArith.auxiliary.Zge_left,Coq.ZArith.auxiliary.Zgt_left,Coq.ZArith.auxiliary.Zlt_left,Coq.ZArith.auxiliary.Zne_left,Coq.micromega.EnvRing.Mphi_ok,Coq.micromega.EnvRing.PNSubst1_ok,Coq.micromega.EnvRing.PNSubst_ok,Coq.micromega.EnvRing.POneSubst_ok,Coq.micromega.EnvRing.PSubstL1_ok,Coq.micromega.EnvRing.PSubstL_ok,Coq.micromega.EnvRing.Padd_ok,Coq.micromega.EnvRing.Pmul_ok,Coq.micromega.EnvRing.Psquare_ok,Coq.micromega.EnvRing.ceqb_spec,Coq.micromega.EnvRing.radd_ext_Proper,Coq.micromega.EnvRing.rmul_ext_Proper,Coq.micromega.OrderedRing.Rle_lt_eq,Coq.micromega.OrderedRing.Rplus_0_l,Coq.micromega.OrderedRing.Rplus_0_r,Coq.micromega.OrderedRing.Rplus_nonneg_nonneg,Coq.micromega.OrderedRing.Rplus_nonneg_pos,Coq.micromega.OrderedRing.Rplus_pos_nonneg,Coq.micromega.OrderedRing.Rplus_pos_pos,Coq.micromega.OrderedRing.Rtimes_0_l,Coq.micromega.OrderedRing.Rtimes_0_r,Coq.micromega.OrderedRing.Rtimes_neq_0,Coq.micromega.OrderedRing.Rtimes_nonneg_nonneg,Coq.micromega.OrderedRing.Rtimes_pos_pos,Coq.micromega.OrderedRing.Rtimes_square_nonneg,Coq.micromega.OrderedRing.SORrt,Coq.micromega.OrderedRing.SORsetoid,Coq.micromega.Refl.make_conj_cons,Coq.micromega.Refl.make_conj_in,Coq.micromega.Refl.not_make_conj_cons,Coq.micromega.RingMicromega.OpAdd_sound,Coq.micromega.RingMicromega.OpMult_sound,Coq.micromega.RingMicromega.Psatz_ind,Coq.micromega.RingMicromega.Rops_wd,Coq.micromega.RingMicromega.SORrm,Coq.micromega.RingMicromega.cltb_sound,Coq.micromega.RingMicromega.eval_Psatz_Sound,Coq.micromega.RingMicromega.eval_pol_add,Coq.micromega.RingMicromega.extract_hyps_app,Coq.micromega.RingMicromega.micomega_sor_setoid,Coq.micromega.RingMicromega.micomega_sor_setoid_Reflexive,Coq.micromega.RingMicromega.micomega_sor_setoid_Symmetric,Coq.micromega.RingMicromega.micomega_sor_setoid_Transitive,Coq.micromega.RingMicromega.nformula_plus_nformula_correct,Coq.micromega.RingMicromega.nformula_times_nformula_correct,Coq.micromega.RingMicromega.nhyps_of_psatz_correct,Coq.micromega.RingMicromega.pexpr_times_nformula_correct,Coq.micromega.RingMicromega.rle_morph_Proper,Coq.micromega.RingMicromega.rlt_morph_Proper,Coq.micromega.RingMicromega.rplus_morph_Proper,Coq.micromega.RingMicromega.rtimes_morph_Proper,Coq.micromega.Tauto.add_term_correct,Coq.micromega.Tauto.eval_cnf_app,Coq.micromega.Tauto.no_middle_eval_tt,Coq.micromega.Tauto.or_clause_cnf_correct,Coq.micromega.Tauto.or_clause_correct,Coq.micromega.Tauto.or_cnf_correct,Coq.micromega.ZMicromega.Vars.Facts.MP.cardinal_inv_1,Coq.micromega.ZMicromega.Vars.Facts.MP.empty_is_empty_1,Coq.micromega.ZMicromega.Vars.Facts.MP.empty_is_empty_2,Coq.micromega.ZMicromega.Vars.Facts.choose_mem_1,Coq.micromega.ZMicromega.Vars.Facts.choose_mem_2,Coq.micromega.ZMicromega.Vars.Facts.choose_mem_4,Coq.micromega.ZMicromega.ZSORaddon,Coq.micromega.ZMicromega.Zdivide_ceiling,Coq.micromega.ZMicromega.Zgcd_pol_correct_lt,Coq.micromega.ZMicromega.Zsor,Coq.micromega.ZMicromega.cutting_plane_sound,Coq.micromega.ZMicromega.eval_Psatz_sound,Coq.micromega.ZMicromega.eval_pol_add,Coq.omega.OmegaLemmas.OMEGA17,Coq.omega.OmegaLemmas.OMEGA2,Coq.omega.OmegaLemmas.OMEGA6,Coq.omega.OmegaLemmas.fast_OMEGA13,Coq.omega.OmegaLemmas.fast_OMEGA15,Coq.omega.OmegaLemmas.fast_Zopp_eq_mult_neg_1,Coq.omega.OmegaLemmas.fast_Zopp_plus_distr,Coq.omega.OmegaLemmas.fast_Zplus_assoc,Coq.omega.OmegaLemmas.fast_Zplus_assoc_reverse,Coq.omega.OmegaLemmas.fast_Zplus_comm,Coq.omega.OmegaLemmas.fast_Zplus_permute,Coq.omega.OmegaLemmas.fast_Zred_factor0,Coq.omega.OmegaLemmas.fast_Zred_factor2,Coq.omega.OmegaLemmas.fast_Zred_factor3,Coq.omega.OmegaLemmas.fast_Zred_factor5,Coq.omega.OmegaLemmas.fast_Zred_factor6,Coq.omega.OmegaLemmas.intro_Z,Coq.omega.OmegaLemmas.new_var,Coq.setoid_ring.Ring_polynom.Mphi_ok,Coq.setoid_ring.Ring_polynom.PNSubst1_ok,Coq.setoid_ring.Ring_polynom.PNSubst_ok,Coq.setoid_ring.Ring_polynom.POneSubst_ok,Coq.setoid_ring.Ring_polynom.PSubstL1_ok,Coq.setoid_ring.Ring_polynom.PSubstL_ok,Coq.setoid_ring.Ring_polynom.Padd_ok,Coq.setoid_ring.Ring_polynom.Peq_ok,Coq.setoid_ring.Ring_polynom.Pmul_ok,Coq.setoid_ring.Ring_polynom.Pol_ind,Coq.setoid_ring.Ring_polynom.Pphi0,Coq.setoid_ring.Ring_polynom.Pphi_ext,Coq.setoid_ring.Ring_polynom.ceqb_spec,Coq.setoid_ring.Ring_polynom.mkVmon_ok,Coq.setoid_ring.Ring_polynom.mkZmon_ok,Coq.setoid_ring.Ring_polynom.mon_of_pol_ok,Coq.setoid_ring.Ring_polynom.radd_ext_Proper,Coq.setoid_ring.Ring_polynom.rmul_ext_Proper,Coq.setoid_ring.Ring_theory.ARadd_0_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.Rth_ARth,Coq.setoid_ring.Ring_theory.mksign_th,Coq.setoid_ring.Ring_theory.morph0,Coq.setoid_ring.Ring_theory.morph1,Coq.setoid_ring.Ring_theory.morph_eq,Coq.setoid_ring.Ring_theory.sign_spec,$adef_Coq.FSets.FSetPositive.PositiveSet.xfold_$a5,$adef_Coq.Arith.PeanoNat.Nat.eqf_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.eq_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.omap_$a2,$adef_$_let_var_var_var_var_var_var_17_QP'_3676_3693_3708_3740_3745_3749_3769_$a8,$adef_Coq.Reals.Rdefinitions.IZR_$a1,$adef_$_lam_206374_$a3,$adef_Coq.micromega.RingMicromega.nformula_times_nformula_$a8,$adef_Coq.FSets.FMapPositive.PositiveMap.remove_$a3,$adef_Coq.Init.Datatypes.None_$a1,$adef_Coq.NArith.BinNat.N.lt_$a2,$adef_Coq.Vectors.VectorDef.cons_$a4,$adef_Coq.ZArith.BinIntDef.Z.of_N_$a1,$adef_Coq.setoid_ring.Ring_polynom.Pequiv_$a9,$adef_Coq.micromega.ZMicromega.eval_nformula_$a2,$adef_Coq.Init.Datatypes.BoolSpec_$a3,$adef_Color.nodemap_$a1,$adef_$_lam_206585_$a4,$adef_Coq.micromega.Tauto.eval_opt_clause_$a6,$adef_Coq.micromega.RingMicromega.PsatzMulC_$a3,$adef_$_lam_41984_$a3,$adef_Coq.micromega.RingMicromega.eval_pol_$a5,$adef_Coq.micromega.ZMicromega.genCuttingPlane_$a1,$adef_Coq.micromega.RingMicromega.psubC_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEc_$a2,$adef_$_case_Coq.Init.Datatypes.prod$140898_$a9,$adef_Coq.FSets.FMapPositive.PositiveMap.xmap2_r_$a5,$adef_Coq.micromega.EnvRing.Pol_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.inter_$a2,$adef_Coq.micromega.Tauto.eval_tt_$a5,$adef_Coq.micromega.Tauto.Cj_$a6,$adef_Coq.setoid_ring.Ring_polynom.PEmul_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.min_elt_$a1,$adef_Coq.FSets.FMapPositive.append_$a2,$adef_Coq.Init.Datatypes.Some_$a1,$adef_Coq.Lists.List.nth_error_$a3,$adef_Coq.setoid_ring.Ring_polynom.Pc_$a2,$adef_$_lam_150690_$a3,$adef_Coq.Init.Nat.log2_iter_$a4,$adef_Coq.setoid_ring.Ring_polynom.vmon_$a2,$adef_$_lam_152789_$a6,$adef_Coq.FSets.FMapPositive.PositiveMap.fold_$a5,$adef_Coq.micromega.EnvRing.POneSubst_$a9,$adef_Coq.Init.Decimal.Pos_$a1,$adef_Coq.setoid_ring.BinList.nth_$a4,$adef_Coq.FSets.FSetPositive.PositiveSet.mem_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pol_$a1,$adef_Coq.Reals.Rdefinitions.IPR_$a1,$adef_Coq.micromega.Env.Env_$a1,$adef_Coq.micromega.EnvRing.Psquare_$a7,$adef_$_lam_41777_$a2,$adef_Coq.Init.Datatypes.CompareSpecT_$a4,$adef_$_case_Coq.Init.Datatypes.bool$186520_$a2,$adef_Coq.setoid_ring.Field_theory.FEdiv_$a3,$adef_Coq.Logic.FinFun.bSurjective_$a2,$adef_Coq.Init.Nat.compare_$a2,$adef_Color.undirected_$a1,$adef_Coq.micromega.EnvRing.Pmul_$a8,$adef_Coq.micromega.ZMicromega.ceiling_$a2,$adef_Coq.setoid_ring.Ring_theory.almost_ring_theory_$a8,$adef_Coq.micromega.Tauto.eval_f_$a7,$adef_Coq.Init.Datatypes.app_$a3,$adef_Coq.Init.Decimal.D6_$a1,$adef_Coq.Init.Specif.value_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.singleton_$a1,$adef_Coq.Init.Specif.sig_$a2,$adef_Color.select_F_$a3,$adef_Coq.micromega.ZMicromega.eval_Psatz_$a2,$adef_$_lam_194304_$a1,$adef_Coq.micromega.EnvRing.Padd_$a6,$adef_Coq.ZArith.BinIntDef.Z.leb_$a2,$adef_Coq.PArith.BinPosDef.Pos.pred_double_$a1,$adef_Coq.setoid_ring.Field_theory.FEmul_$a3,$adef_$_case_Coq.Init.Datatypes.prod$147444_$a15,$adef_Coq.ZArith.BinIntDef.Z.mul_$a2,$adef_Coq.Arith.PeanoNat.Nat.Private_Tac.interp_ord_$a1,$adef_Coq.Init.Decimal.D4_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.Equal_$a2,$adef_Coq.micromega.RingMicromega.Build_Formula_$a4,$adef_Coq.Init.Specif.sumbool_$a2,$adef_Color.WP.Add_$a5,$adef_Coq.setoid_ring.Field_theory.mk_rsplit_$a4,$adef_Coq.Strings.Byte.to_N_$a1,$adef_Coq.micromega.EnvRing.PNSubst1_$a10,$adef_Coq.micromega.EnvRing.PsubC_$a2,$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.FSets.FMapPositive.PositiveMap._map2_$a4,$adef_Coq.micromega.Env.jump_$a3,$adef_Coq.setoid_ring.Ring_polynom.PNSubst_$a11,$adef_Coq.Init.Nat.max_$a2,$adef_Coq.Strings.Ascii.N_of_digits_$a1,$adef_Coq.Lists.List.hd_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.cardinal_$a1,$adef_Coq.FSets.FMapPositive.PositiveMap.Node_$a4,$adef_Coq.Init.Datatypes.option_$a1,$adef_Coq.Strings.Byte.of_nat_$a1,$adef_Coq.Relations.Relation_Definitions.relation_$a1,$adef_Coq.setoid_ring.Ring_polynom.Pphi_$a8,$adef_Coq.setoid_ring.Ring_polynom.Peq_$a4,$adef_Coq.Structures.OrderedType.LT_$a5,$adef_Coq.Vectors.VectorDef.t_$a2,$adef_Coq.setoid_ring.Ring_polynom.PExpr_$a1,$adef_Coq.Init.Datatypes.orb_$a2,$adef_$_prop_26965_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_morph_$a17,$adef_Coq.Init.Datatypes.CompOpp_$a1,$adef_$_lam_150706_$a4,$adef_Coq.micromega.EnvRing.PEopp_$a2,$adef_Coq.setoid_ring.Ring_polynom.PaddC_$a4,$adef_$_lam_150690_$a4,$adef_Coq.micromega.RingMicromega.SORaddon_$a22,$adef_Coq.FSets.FMapPositive.PositiveMap.find_$a3,$adef_Coq.setoid_ring.Field_theory.FExpr_$a1,$adef_Coq.micromega.ZMicromega.eval_nformula_$a1,$adef_$_lam_150714_$a4,$adef_Coq.micromega.RingMicromega.PolEnv_$a1,$adef_$_let_var_var_var_var_var_var_15_QQ'_145099_145115_145130_145162_145167_145171_145187_$a8,$adef_Coq.setoid_ring.Ring_polynom.MPcond_$a10,$adef_Coq.micromega.Tauto.or_clause_cnf_$a6,$adef_Coq.micromega.Tauto.and_cnf_$a4,$adef_Coq.FSets.FMapPositive.PositiveMap.cardinal_$a1,$adef_Coq.micromega.Tauto.eval_cnf_$a6,$adef_Coq.micromega.Tauto.cnf_ff_$a2,$adef_Coq.Strings.Ascii.N_of_ascii_$a1,$adef_Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.interp_ord_$a1,$adef_Coq.micromega.EnvRing.zmon_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pmul_$a8,$adef_Coq.setoid_ring.Ring_polynom.mkPinj_$a3,$adef_Coq.Arith.Between.in_int_$a3,$adef_Coq.setoid_ring.Ring_theory.div_theory_$a7,$adef_Coq.Init.Datatypes.inl_$a3,$adef_Coq.setoid_ring.Ring_polynom.mkZmon_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.remove_$a1,$adef_Coq.Strings.String.length_$a1,$adef_Coq.setoid_ring.Ring_theory.ring_eq_ext_$a5,$adef_Coq.micromega.RingMicromega.cltb_$a5,$adef_Coq.setoid_ring.Ring_polynom.Pphi_$a6,$adef_Coq.FSets.FMapPositive.PositiveMap.tree_$a1,$adef_Color.low_deg_$a3,$adef_Coq.Init.Datatypes.nil_$a1,$adef_Color.WP.Partition_$a4,$adef_Coq.FSets.FMapPositive.PositiveMap.MapsTo_$a4,$adef_$_lam_2569_$a1,$adef_Coq.Logic.FinFun.bFun_$a2,$adef_Coq.Init.Datatypes.CompGtT_$a3,$adef_$_lam_150698_$a4,$adef_Coq.micromega.Tauto.GFormula_$a4,$adef_Coq.micromega.Tauto.cnf_$a2,$adef_Coq.Numbers.BinNums.Npos_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.node_$a3,$adef_$_lam_209153_$a4,$adef_Coq.setoid_ring.Ring_polynom.P0_$a2,$adef_Coq.micromega.EnvRing.PmulC_aux_$a6,$adef_Coq.micromega.Tauto.add_term_$a6,$adef_Coq.micromega.RingMicromega.OpMult_$a2,$adef_$_lam_26889_$a1,$adef_Coq.Numbers.BinNums.xI_$a1,$adef_Coq.micromega.EnvRing.MFactor_$a5,$adef_$_lam_209153_$a6,$adef_Coq.Init.Decimal.D1_$a1,$adef_$_prop_187906_$a2,$adef_Coq.micromega.RingMicromega.eval_Psatz_$a7,$adef_Coq.Init.Nat.div2_$a1,$adef_Coq.Init.Datatypes.negb_$a1,$adef_Coq.Init.Nat.log2_$a1,$adef_Coq.Init.Nat.testbit_$a2,$adef_Coq.Reals.Rdefinitions.Ropp_$a1,$adef_Coq.Strings.Byte.to_nat_$a1,$adef_Coq.setoid_ring.Ring_polynom.PEeval_$a14,$adef_$_let_var_var_var_var_var_var_16_PQ'_145098_145114_145129_145161_145166_145170_145188_$a8,$adef_Coq.ZArith.BinIntDef.Z.succ_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.add_$a2,$adef_Coq.Init.Nat.add_$a2,$adef_Coq.Structures.OrderedType.Compare_$a5,$adef_$_let_var_6_p_22552_22555_$a4,$adef_Coq.setoid_ring.Field_theory.FEc_$a2,$adef_Coq.Classes.Morphisms.Proper_$a3,$adef_$_fix_2314_1_add_carry_$a2,$adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2,$adef_Coq.Init.Nat.ltb_$a2,$adef_Coq.micromega.EnvRing.mkPX_$a6,$adef_Coq.Init.Specif.right_$a2,$adef_Coq.setoid_ring.Ring_theory.power_theory_$a7,$adef_Coq.Lists.List.fold_left_$a5,$adef_Coq.micromega.Env.hd_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.max_elt_$a1,$adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3,$adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2,$adef_Coq.FSets.FMapPositive.PositiveMap.xelements_$a3,$adef_Coq.Lists.List.rev_$a2,$adef_Coq.setoid_ring.Field_theory.FEadd_$a3,$adef_Coq.Init.Datatypes.S_$a1,$adef_Coq.Strings.Ascii.Ascii_$a8,$adef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_$a2,$adef_Coq.micromega.EnvRing.PEpow_$a3,$adef_Coq.setoid_ring.Ring_polynom.zmon_$a2,$adef_Coq.ZArith.BinIntDef.Z.add_$a2,$adef_Coq.micromega.EnvRing.Peq_$a4,$adef_Coq.micromega.RingMicromega.Formula_$a1,$adef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_dec_$a2,$adef_Coq.micromega.RingMicromega.PolC_$a1,$adef_Coq.Strings.Byte.of_N_$a1,$adef_Coq.Lists.SetoidList.InA_$a4,$adef_Coq.micromega.RingMicromega.nformula_plus_nformula_$a6,$adef_Coq.Sorting.Permutation.Permutation_$a3,$adef_Coq.ZArith.BinIntDef.Z.sub_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pequiv_$a7,$adef_Coq.setoid_ring.Ring_polynom.PEopp_$a2,$adef_Coq.Init.Nat.modulo_$a2,$adef_$_lam_152682_$a9,$adef_Coq.setoid_ring.Field_theory.mk_linear_$a4,$adef_Coq.micromega.Env.tail_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pmul_$a6,$adef_Coq.setoid_ring.Ring_theory.pow_pos_$a4,$adef_Coq.Init.Nat.pow_$a2,$adef_Coq.FSets.FMapPositive.PositiveMap.xmap2_l_$a5,$adef_Coq.micromega.Tauto.I_$a7,$adef_Coq.micromega.Refl.make_conj_$a3,$adef_$_case_Coq.Init.Specif.sumbool$28924_$a5,$adef_Coq.ZArith.BinInt.Z.gt_$a2,$adef_Coq.Classes.RelationClasses.Symmetric_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEO_$a1,$adef_Coq.Numbers.BinNums.xO_$a1,$adef_Coq.micromega.RingMicromega.eval_op1_$a7,$adef_$_prop_29976_$a2,$adef_Coq.micromega.EnvRing.Pphi_$a5,$adef_$_let_var_6_p_22554_22556_$a4,$adef_Coq.setoid_ring.Field_theory.FEinv_$a2,$adef_Coq.Init.Wf.Acc_$a3,$adef_$_let_var_var_var_var_var_var_16_PQ'_3678_3694_3709_3741_3746_3750_3768_$a8,$adef_Coq.setoid_ring.Ring_theory.pow_N_$a5,$adef_Coq.setoid_ring.Ring_polynom.PmulC_aux_$a6,$adef_Coq.NArith.BinNatDef.N.of_nat_$a1,$adef_Coq.Init.Decimal.D8_$a1,$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.FSets.FMapPositive.PositiveMap.xfind_$a4,$adef_Coq.micromega.OrderedRing.SOR_$a10,$adef_Coq.Init.Nat.sqrt_$a1,$adef_Coq.Init.Datatypes.sum_$a2,$adef_Coq.ZArith.Znumtheory.Zis_gcd_$a3,$adef_Coq.Lists.SetoidList.findA_$a4,$adef_Coq.Vectors.Fin.t_$a1,$adef_Coq.setoid_ring.Ring_polynom.PSubstL_$a10,$adef_Coq.setoid_ring.Field_theory.FEO_$a1,$adef_$_let_var_var_var_var_var_var_18_PP'_145094_145111_145126_145158_145164_145168_145190_$a8,$adef_Coq.Lists.List.In_$a3,$adef_Coq.Init.Datatypes.option_map_$a4,$adef_Coq.FSets.FSetPositive.PositiveSet.Empty_$a1,$adef_Coq.FSets.FMapPositive.PositiveMap.map_$a4,$adef_Coq.Init.Datatypes.andb_$a2,$adef_Coq.Init.Peano.lt_$a2,$adef_Coq.micromega.ZMicromega.nformula_of_cutting_plane_$a1,$adef_Coq.setoid_ring.Ring_theory.pow_N_$a3,$adef_Coq.PArith.BinPos.Pos.le_$a2,$adef_Coq.Init.Nat.mul_$a2,$adef_Coq.Init.Decimal.D7_$a1,$adef_Coq.micromega.Tauto.eval_clause_$a5,$adef_Coq.FSets.FSetPositive.PositiveSet.Node_$a3,$adef_Coq.Init.Peano.le_$a2,$adef_Coq.setoid_ring.Field_theory.rsplit_$a1,$adef_Coq.Init.Decimal.D2_$a1,$adef_Coq.Logic.FinFun.Injective_$a3,$adef_$_lam_206585_$a1,$adef_Coq.Classes.RelationClasses.Equivalence_$a2,$adef_Coq.micromega.Tauto.TT_$a4,$adef_Coq.Logic.Decidable.decidable_$a1,$adef_Coq.micromega.ZMicromega.ZgcdM_$a2,$adef_Coq.micromega.EnvRing.PEmul_$a3,$adef_Coq.Init.Datatypes.snd_$a3,$adef_Coq.micromega.RingMicromega.OpAdd_$a2,$adef_Coq.PArith.BinPos.Pos.lt_$a2,$adef_Coq.ZArith.BinIntDef.Z.gcd_$a2,$adef_Coq.Init.Decimal.D0_$a1,$adef_Coq.PArith.BinPosDef.Pos.to_nat_$a1,$adef_Coq.setoid_ring.Ring_polynom.PmulI_$a9,$adef_Coq.FSets.FSetPositive.PositiveSet.choose_$a1,$adef_Coq.Init.Datatypes.CompLtT_$a3,$adef_Coq.Lists.List.nth_$a4,$adef_Coq.micromega.EnvRing.Padd_$a4,$adef_Coq.Lists.SetoidList.transpose_$a4,$adef_Color.nodes_$a1,$adef_$_prop_187904_$a2,$adef_Coq.micromega.EnvRing.Pphi_$a7,$adef_Coq.setoid_ring.Ring_polynom.zmon_pred_$a2,$adef_Coq.micromega.EnvRing.mkPinj_$a3,$adef_Coq.setoid_ring.Ring_polynom.PNSubst1_$a11,$adef_Coq.FSets.FMapPositive.PositiveMap.mapi_$a4,$adef_Coq.Init.Datatypes.inr_$a3,$adef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.lt_$a2,$adef_Coq.micromega.EnvRing.MPcond_$a9,$adef_Coq.Vectors.Fin.F1_$a1,$adef_Color.subset_nodes_$a2,$adef_$_lam_60496_$a1,$adef_Coq.micromega.RingMicromega.padd_$a4,$adef_Coq.FSets.FMapPositive.PositiveMap.xfoldi_$a6,$adef_Coq.PArith.BinPosDef.Pos.succ_$a1,$adef_Coq.setoid_ring.Field_theory.FEsub_$a3,$adef_Coq.micromega.ZMicromega.Zgcd_pol_$a1,$adef_$_prop_40945_$a2,$adef_Coq.micromega.Tauto.D_$a6,$adef_$_prop_187905_$a2,$adef_Coq.Init.Datatypes.prod_$a2,$adef_Coq.Init.Datatypes.option_rec_$a2,$adef_Coq.ZArith.BinIntDef.Z.compare_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_theory_$a8,$adef_$_case_Coq.Init.Datatypes.bool$28461_$a4,$adef_Coq.micromega.Tauto.eval_tt_$a6,$adef_Coq.Strings.Ascii.nat_of_ascii_$a1,$adef_Coq.FSets.FMapPositive.PositiveMap.Empty_$a2,$adef_$_lam_60496_$a4,$adef_Coq.micromega.RingMicromega.pexpr_times_nformula_$a8,$adef_Coq.micromega.EnvRing.PaddI_$a6,$adef_$_let_var_var_var_11_twoPQ_150915_150919_150922_150930_$a8,$adef_Coq.Bool.Bool.eqb_$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.micromega.RingMicromega.padd_$a6,$adef_Coq.Arith.PeanoNat.Nat.b2n_$a1,$adef_Coq.micromega.EnvRing.PmulC_$a7,$adef_Coq.Strings.String.prefix_$a2,$adef_Color.low_deg_$a1,$adef_Color.Mdomain_$a2,$adef_$_let_var_var_var_var_var_14_QQ'_3685_3701_3716_3728_3732_3758_$a9,$adef_Coq.ZArith.BinIntDef.Z.opp_$a1,$adef_Coq.FSets.FMapPositive.PositiveMap._map2_$a6,$adef_Coq.Numbers.BinNums.Zneg_$a1,$adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3,$adef_Coq.NArith.BinNatDef.N.to_nat_$a1,$adef_Coq.Classes.RelationClasses.Transitive_$a2,$adef_Coq.FSets.FMapPositive.PositiveMap.eq_key_elt_$a3,$adef_Coq.micromega.EnvRing.Mphi_$a5,$adef_Coq.ZArith.BinIntDef.Z.double_$a1,$adef_Coq.FSets.FMapPositive.PositiveMap.cardinal_$a2,$adef_Coq.Bool.Bool.reflect_$a2,$adef_Coq.setoid_ring.Ring_polynom.PX_$a4,$adef_$_prop_28935_$a3,$adef_Coq.NArith.BinNatDef.N.leb_$a2,$adef_$_lam_206374_$a1,$adef_Coq.setoid_ring.Ring_polynom.Padd_$a4,$adef_Coq.setoid_ring.Ring_polynom.PaddX_$a7,$adef_Coq.micromega.RingMicromega.eval_nformula_$a11,$adef_Coq.micromega.RingMicromega.PsatzIn_$a2,$adef_Coq.Strings.Ascii.ascii_dec_$a2,$adef_Coq.Init.Specif.inright_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEI_$a1,$adef_$_lam_150698_$a3,$adef_Coq.ZArith.BinIntDef.Z.gtb_$a2,$adef_$_lam_194304_$a3,$adef_$_prop_28936_$a3,$adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3,$adef_Coq.FSets.FMapPositive.PositiveMap.mem_$a3,$adef_Coq.micromega.Tauto.cnf_checker_$a6,$adef_Coq.setoid_ring.Field_theory.FEopp_$a2,$adef_Coq.setoid_ring.Ring_polynom.mkPX_$a6,$adef_Coq.micromega.RingMicromega.cneqb_$a4,$adef_Coq.Init.Datatypes.CompareSpec_$a4,$adef_Coq.micromega.RingMicromega.map_option2_$a6,$adef_Coq.Strings.String.String_$a2,$adef_Coq.micromega.Tauto.or_clause_$a6,$adef_Coq.Init.Datatypes.CompEqT_$a3,$adef_Coq.micromega.RingMicromega.extract_hyps_$a4,$adef_Coq.micromega.RingMicromega.PsatzMulE_$a3,$adef_Coq.FSets.FMapPositive.PositiveMap.Leaf_$a1,$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.FSets.FSetPositive.PositiveSet.In_$a2,$adef_Coq.micromega.ZMicromega.padd_$a2,$adef_Coq.Init.Nat.leb_$a2,$adef_Coq.Structures.OrderedType.GT_$a5,$adef_Coq.ZArith.BinIntDef.Z.succ_double_$a1,$adef_Coq.micromega.EnvRing.PSubstL1_$a9,$adef_Coq.micromega.EnvRing.PNSubst_$a10,$adef_Coq.Vectors.Fin.FS_$a2,$adef_Coq.FSets.FMapPositive.PositiveMap.map2_$a4,$adef_Coq.micromega.EnvRing.PExpr_$a1,$adef_Coq.Init.Datatypes.option_rect_$a2,$adef_$_prop_28933_$a3,$adef_$_prop_187903_$a2,$adef_Coq.Setoids.Setoid.Setoid_Theory_$a2,$adef_Coq.setoid_ring.BinList.jump_$a3,$adef_Coq.Init.Peano.ge_$a2,$adef_$_cast_193798_$a1,$adef_Coq.Init.Decimal.Neg_$a1,$adef_Coq.micromega.RingMicromega.nhyps_of_psatz_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.is_empty_$a1,$adef_Coq.micromega.EnvRing.PSubstL_$a9,$adef_Coq.Lists.SetoidList.NoDupA_$a3,$adef_Color.WP.transpose_neqkey_$a4,$adef_$_lam_41777_$a1,$adef_Coq.micromega.RingMicromega.eval_op1_$a6,$adef_Coq.Init.Decimal.D9_$a1,$adef_Coq.setoid_ring.Ring_polynom.Padd_$a6,$adef_Coq.FSets.FSetPositive.PositiveSet.Subset_$a2,$adef_Coq.Classes.RelationClasses.Reflexive_$a2,$adef_Coq.micromega.Tauto.A_$a6,$adef_Coq.micromega.EnvRing.P0_$a2,$adef_Coq.micromega.EnvRing.vmon_$a2,$adef_Coq.micromega.Tauto.X_$a5,$adef_Coq.FSets.FMapPositive.PositiveMap.elements_$a2,$adef_Coq.FSets.FMapPositive.PositiveMap.Equal_$a3,$adef_Coq.setoid_ring.Field_theory.almost_field_theory_$a10,$adef_Coq.Arith.Wf_nat.ltof_$a4,$adef_Coq.Init.Datatypes.option_rect_$a5,$adef_Coq.Init.Specif.sumor_$a2,$adef_Coq.PArith.BinPosDef.Pos.mul_$a2,$adef_Coq.micromega.ZMicromega.eval_pol_$a2,$adef_Coq.Init.Nat.pred_$a1,$adef_Coq.Init.Specif.exist_$a3,$adef_$_lam_150706_$a3,$adef_Coq.micromega.ZMicromega.Zdiv_pol_$a2,$adef_Coq.Strings.String.get_$a2,$adef_$_lam_150714_$a3,$adef_Coq.ZArith.BinInt.Z.le_$a2,$adef_Coq.Strings.String.index_$a3,$adef_$_prop_28934_$a3,$adef_Coq.micromega.ZMicromega.makeCuttingPlane_$a1,$adef_$_prop_143705_$a4,$adef_Coq.Lists.List.map_$a4,$adef_Coq.micromega.EnvRing.PsubC_$a4,$adef_Coq.PArith.BinPosDef.Pos.compare_cont_$a1,$adef_Coq.micromega.EnvRing.Pmul_$a6,$adef_Coq.setoid_ring.Ring_polynom.Mphi_$a6,$adef_Coq.Init.Specif.inleft_$a3,$adef_Coq.micromega.EnvRing.Pinj_$a3,$adef_Coq.Init.Wf.well_founded_$a2,$adef_Coq.Init.Datatypes.cons_$a3,$adef_Coq.micromega.RingMicromega.PsatzSquare_$a2,$adef_Coq.FSets.FMapPositive.PositiveMap.add_$a4,$adef_$_case_Coq.Init.Datatypes.prod$207653_$a12,$adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1,$adef_Coq.Init.Datatypes.pair_$a4,$adef_Coq.ZArith.BinIntDef.Z.pred_double_$a1,$adef_$_prop_26964_$a2,$adef_Coq.micromega.Tauto.cnf_tt_$a2,$adef_Coq.Init.Nat.sqrt_iter_$a4,$adef_Coq.FSets.FSetPositive.PositiveSet.union_$a2,$adef_$_lam_152789_$a7,$adef_Coq.PArith.BinPosDef.Pos.max_$a2,$adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a2,$adef_Coq.micromega.RingMicromega.Psatz_$a1,$adef_$_lam_152682_$a8,$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.Lists.List.find_$a3,$adef_Coq.setoid_ring.Ring_polynom.POneSubst_$a10,$adef_$_let_var_var_var_var_var_var_15_QQ'_3679_3695_3710_3742_3747_3751_3767_$a8,$adef_Coq.Init.Datatypes.list_$a1,$adef_Color.adj_$a2,$adef_Coq.setoid_ring.Ring_polynom.mkVmon_$a2,$adef_Coq.Init.Nat.sub_$a2,$adef_Coq.micromega.Tauto.clause_$a2,$adef_Coq.micromega.RingMicromega.eval_Psatz_$a9,$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.setoid_ring.Field_theory.FEI_$a1,$adef_Coq.micromega.EnvRing.PEX_$a2,$adef_Coq.Bool.Bool.ReflectT_$a1,$adef_Coq.micromega.EnvRing.PmulI_$a9,$adef_$_let_var_var_var_12_Q2_150916_150920_150923_150931_$a7,$adef_Coq.micromega.EnvRing.PaddC_$a4,$adef_Color.no_selfloop_$a1,$adef_Coq.Init.Decimal.D5_$a1,$adef_Coq.setoid_ring.Ring_polynom.PmulC_$a7,$adef_Coq.NArith.BinNatDef.N.compare_$a2,$adef_Coq.Lists.List.hd_error_$a2,$adef_Coq.Init.Datatypes.fst_$a3,$adef_Coq.setoid_ring.Ring_polynom.mon_of_pol_$a4,$adef_$_let_var_var_var_var_var_var_17_QP'_145096_145113_145128_145160_145165_145169_145189_$a8,$adef_Coq.micromega.Tauto.or_cnf_$a6,$adef_Coq.FSets.FMapPositive.PositiveMap.map2_$a6,$adef_Coq.micromega.RingMicromega.PsatzAdd_$a3,$adef_Coq.FSets.FMapPositive.PositiveMap.Equal_$a1,$adef_Coq.setoid_ring.Ring_polynom.PSubstL1_$a10,$adef_Coq.micromega.Tauto.N_$a5,$adef_Coq.setoid_ring.Ring_polynom.MFactor_$a8,$adef_Coq.ZArith.Znat.neq_$a2,$adef_Coq.Strings.String.substring_$a3,$adef_Coq.Init.Nat.min_$a2,$adef_Coq.micromega.RingMicromega.PsatzC_$a2,$adef_Coq.ZArith.BinInt.Zne_$a2,$adef_Coq.PArith.BinPosDef.Pos.compare_$a2,$adef_Coq.ZArith.BinIntDef.Z.div_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.remove_$a2,$adef_Coq.micromega.RingMicromega.PsatzZ_$a1,$adef_Coq.FSets.FMapPositive.PositiveMap.In_$a3,$adef_Coq.micromega.Tauto.eval_clause_$a6,$adef_Coq.Lists.List.fold_right_$a5,$adef_Coq.micromega.EnvRing.PaddX_$a7,$adef_Coq.Init.Nat.odd_$a1,$adef_$_let_var_var_var_13_P2_150913_150918_150921_150932_$a7,$adef_Coq.Lists.List.tl_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.equal_$a2,$adef_Coq.FSets.FMapPositive.PositiveMap.t_$a1,$adef_Coq.setoid_ring.Ring_theory.sign_theory_$a4,$adef_$_lam_41984_$a4,$adef_Coq.Logic.FinFun.bInjective_$a2,$adef_Coq.setoid_ring.Field_theory.FEX_$a2,$adef_Coq.setoid_ring.Ring_polynom.PaddI_$a6,$adef_Color.WP.Disjoint_$a3,$adef_Coq.Lists.List.NoDup_$a2,$adef_Coq.Vectors.VectorDef.nil_$a1,$adef_Coq.Init.Specif.left_$a2,$adef_$_let_var_var_var_var_var_14_QQ'_145105_145121_145136_145148_145152_145178_$a9,$adef_Coq.micromega.RingMicromega.map_option_$a4,$adef_Coq.Init.Decimal.D3_$a1,$adef_Coq.micromega.RingMicromega.NFormula_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.fold_$a4,$adef_$_case_Coq.Init.Datatypes.bool$39205_$a2,$adef_Coq.ZArith.BinIntDef.Z.pow_$a2,$adef_Coq.micromega.EnvRing.PX_$a4,$adef_Coq.micromega.EnvRing.PEadd_$a3,$adef_Coq.setoid_ring.Field_theory.FEpow_$a3,$adef_Coq.Init.Datatypes.length_$a2,$adef_Color.remove_node_$a2,$adef_Coq.micromega.ZMicromega.is_diff_env_elt_$a4,$adef_$_let_var_var_var_var_var_var_18_PP'_3674_3691_3706_3738_3744_3748_3770_$a8,$adef_Coq.micromega.RingMicromega.eval_pol_$a7,$adef_Coq.Init.Nat.divmod_$a4,$adef_Coq.PArith.BinPosDef.Pos.of_succ_nat_$a1,$adef_Coq.micromega.EnvRing.PEsub_$a3,$adef_Coq.micromega.RingMicromega.eval_nformula_$a9,$adef_Coq.PArith.BinPosDef.Pos.add_$a2,$adef_Coq.Init.Peano.gt_$a2,$tdef_$_type_27428,$tdef_$_type_206598,$tdef_$_type_37430,$tdef_$_type_34039,$tdef_Coq.FSets.FMapPositive.PositiveMap.key,$tdef_$_type_145246,$tdef_$_type_25048,$tdef_$_type_23021,$tdef_$_type_140643,$tdef_$_type_152513,$tdef_$_type_150446,$tdef_$_type_206568,$tdef_$_type_9671,$tdef_$_type_23836,$tdef_$_type_26627,$tdef_$_type_42262,$tdef_$_type_19049,$tdef_$_type_28478,$tdef_$_type_23782,$tdef_Coq.Init.Datatypes.bool,$tdef_$_type_47342,$tdef_$_type_27113,$tdef_$_type_2301,$tdef_Coq.Structures.OrdersTac.ord,$tdef_Coq.micromega.EnvRing.PExpr,$tdef_$_type_140911,$tdef_$_type_152817,$tdef_$_type_37450,$tdef_$_type_208170,$tdef_$_type_23806,$tdef_$_type_206565,$tdef_$_type_208957,$tdef_$_type_18960,$tdef_$_type_761,$tdef_$_type_38871,$tdef_$_type_26503,$tdef_$_type_3370,$tdef_$_type_11489,$tdef_$_type_4422,$tdef_$_type_35077,$tdef_$_type_22841,$tdef_$_type_30779,$tdef_Color.nodemap,$tdef_Coq.Init.Datatypes.comparison,$tdef_Coq.setoid_ring.Ring_polynom.Mon,$tdef_$_type_802,$tdef_$_type_32021,$tdef_$_type_30051,$tdef_$_type_25900,$tdef_$_type_39577,$tdef_$_type_144054,$tdef_Coq.micromega.Tauto.GFormula,$tdef_$_type_135373,$tdef_$_type_29392,$tdef_$_type_3656,$tdef_$_type_506,$tdef_$_type_141336,$tdef_$_type_206819,$tdef_Coq.Init.Specif.sumbool,$tdef_$_type_30974,$tdef_$_type_38777,$tdef_$_type_168,$tdef_$_type_624,$tdef_$_type_206943,$tdef_$_type_38791,$tdef_$_type_570,$tdef_$_type_23752,$tdef_$_type_60800,$tdef_$_type_55311,$tdef_$_type_146123,$tdef_$_type_471,$tdef_$_type_144641,$tdef_$_type_710,$tdef_$_type_683,$tdef_$_type_209029,$tdef_Coq.setoid_ring.Field_theory.FExpr,$tdef_$_type_206591,$tdef_$_type_3489,$tdef_$_type_193820,$tdef_$_type_154688,$tdef_$_type_31619,$tdef_$_type_150673,$tdef_Coq.micromega.RingMicromega.PolEnv,$tdef_$_type_3540,$tdef_$_type_27043,$tdef_$_type_1070,$tdef_$_type_150981,$tdef_$_type_30905,$tdef_Coq.Init.Specif.sig,$tdef_$_type_41347,$tdef_$_type_145067,$tdef_$_type_597,$tdef_Coq.Strings.Ascii.ascii,$tdef_$_type_2344,$tdef_$_type_4329,$tdef_$_type_56096,$tdef_$_type_31673,$tdef_$_type_36438,$tdef_Coq.Relations.Relation_Definitions.relation,$tdef_$_type_33024,$tdef_$_type_135700,$tdef_$_type_8078,$tdef_$_type_206780,$tdef_$_type_152508,$tdef_$_type_26962,$tdef_$_type_725,$tdef_$_type_44845,$tdef_$_type_27516,$tdef_$_type_31712,$tdef_$_type_152738,$tdef_$_type_49,$tdef_$_type_60798,$tdef_$_type_141644,$tdef_$_type_135379,$tdef_$_type_43295,$tdef_Coq.micromega.RingMicromega.Op2,$tdef_$_type_678,$tdef_$_type_28483,$tdef_Coq.Init.Byte.byte,$tdef_$_type_37084,$tdef_Coq.Init.Decimal.int,$tdef_$_type_39208,$tdef_$_type_27144,$tdef_$_type_28348,$tdef_$_type_31939,$tdef_$_type_18965,$tdef_Coq.Strings.String.string,$tdef_Coq.FSets.FMapPositive.PositiveMap.tree,$tdef_$_type_41993,$tdef_$_type_2390,$tdef_$_type_4031,$tdef_$_type_33693,$tdef_$_type_39104,$tdef_$_type_207018,$tdef_$_type_595,$tdef_$_type_54401,$tdef_$_type_19055,$tdef_$_type_4772,$tdef_$_type_39078,$tdef_$_type_206793,$tdef_$_type_60622,$tdef_$_type_27353,$tdef_$_type_194701,$tdef_$_type_30859,$tdef_$_type_35746,$tdef_$_type_206811,$tdef_Color.nodeset,$tdef_$_type_31946,$tdef_$_type_27417,$tdef_$_type_27361,$tdef_$_type_31648,$tdef_$_type_28492,$tdef_$_type_907,$tdef_$_type_206782,$tdef_$_type_35423,$tdef_$_type_134676,$tdef_$_type_34731,$tdef_$_type_26641,$tdef_$_type_10623,$tdef_Coq.Structures.OrderedType.Compare,$tdef_Coq.Init.Specif.sumor,$tdef_$_type_38767,$tdef_$_type_31970,$tdef_$_type_30909,$tdef_$_type_19352,$tdef_$_type_146557,$tdef_$_type_25687,$tdef_$_type_144962,$tdef_$_type_54616,$tdef_$_type_144633,$tdef_$_type_11656,$tdef_Coq.micromega.Tauto.cnf,$tdef_$_type_26308,$tdef_$_type_29167,$tdef_$_type_2004,$tdef_$_type_36092,$tdef_$_type_18973,$tdef_$_type_197185,$tdef_Coq.Numbers.BinNums.Z,$tdef_Coq.QArith.QArith_base.Q,$tdef_$_type_1995,$tdef_Coq.Numbers.BinNums.positive,$tdef_$_type_4597,$tdef_Coq.Init.Datatypes.nat,$tdef_$_type_9662,$tdef_$_type_37454,$tdef_$_type_27051,$tdef_$_type_53755,$tdef_$_type_40333,$tdef_$_type_207068,$tdef_$_type_24427,$tdef_Coq.Init.Datatypes.prod,$tdef_$_type_22566,$tdef_$_type_149684,$tdef_$_type_4040,$tdef_Coq.micromega.RingMicromega.Formula,$tdef_$_type_3826,$tdef_$_type_19706,$tdef_$_type_8057,$tdef_$_type_27563,$tdef_$_type_1338,$tdef_Coq.micromega.Tauto.clause,$tdef_$_type_60498,$tdef_$_type_135002,$tdef_Coq.Vectors.VectorDef.t,$tdef_$_type_149784,$tdef_$_type_32039,$tdef_$_type_27077,$tdef_$_type_23866,$tdef_$_type_206714,$tdef_$_type_1511,$tdef_$_type_9685,$tdef_$_type_141004,$tdef_$_type_520,$tdef_$_type_194742,$tdef_$_type_59359,$tdef_$_type_163,$tdef_Coq.Vectors.Fin.t,$tdef_$_type_38950,$tdef_$_type_155137,$tdef_$_type_1044,$tdef_$_type_28399,$tdef_$_type_29310,$tdef_$_type_10421,$tdef_$_type_656,$tdef_$_type_1344,$tdef_Coq.micromega.Env.Env,$tdef_Coq.micromega.RingMicromega.Psatz,$tdef_$_type_33370,$tdef_$_type_550,$tdef_$_type_31657,$tdef_Coq.micromega.EnvRing.Mon,$tdef_$_type_12,$tdef_$_type_26095,$tdef_$_type_378,$tdef_$_type_11645,$tdef_$_type_11650,$tdef_$_type_738,$tdef_$_type_141079,$tdef_$_type_206562,$tdef_$_type_3304,$tdef_$_type_24640,$tdef_Coq.Init.Datatypes.list,$tdef_$_type_29352,$tdef_$_type_30881,$tdef_$_type_152516,$tdef_$_type_11658,$tdef_Coq.Init.Datatypes.option,$tdef_$_type_42004,$tdef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$tdef_$_type_208948,$tdef_$_type_140693,$tdef_$_type_1041,$tdef_Coq.FSets.FSetPositive.PositiveSet.elt,$tdef_$_type_632,$tdef_$_type_193771,$tdef_$_type_206816,$tdef_$_type_124,$tdef_$_type_137608,$tdef_$_type_530,$tdef_$_type_137465,$tdef_$_type_1033,$tdef_$_type_31653,$tdef_$_type_153912,$tdef_$_type_149503,$tdef_$_type_30815,$tdef_$_type_26959,$tdef_$_type_2012,$tdef_$_type_29285,$tdef_$_type_41152,$tdef_Coq.Numbers.BinNums.N,$tdef_$_type_518,$tdef_$_type_1039,$tdef_$_type_23947,$tdef_$_type_27366,$tdef_$_type_145995,$tdef_$_type_209098,$tdef_$_type_2265,$tdef_$_type_53787,$tdef_$_type_2742,$tdef_$_type_193292,$tdef_$_type_47286,$tdef_$_type_206573,$tdef_Coq.Reals.Rdefinitions.R,$tdef_Color.node,$tdef_$_type_155161,$tdef_Coq.micromega.ZMicromega.ZWitness,$tdef_$_type_25261,$tdef_$_type_47339,$tdef_$_type_1522,$tdef_$_type_26608,$tdef_$_type_150420,$tdef_$_type_144757,$tdef_$_type_36761,$tdef_$_type_150809,$tdef_$_type_141435,$tdef_$_type_40740,$tdef_Coq.FSets.FSetPositive.PositiveSet.t,$tdef_$_type_206605,$tdef_Coq.Init.Datatypes.unit,$tdef_$_type_22904,$tdef_$_type_209214,$tdef_$_type_47431,$tdef_$_type_34385,$tdef_$_type_144561,$tdef_Coq.Init.Datatypes.sum,$tdef_$_type_2567,$tdef_$_type_23890,$tdef_$_type_193265,$tdef_$_type_137619,$tdef_Coq.FSets.FSetPositive.PositiveSet.tree,$tdef_$_type_2672,$tdef_$_type_193283,$tdef_$_type_38837,$tdef_$_type_3102,$tdef_$_type_26868,$tdef_$_type_146242,$tdef_$_type_143703,$tdef_$_type_152615,$tdef_Coq.setoid_ring.Field_theory.linear,$tdef_$_type_750,$tdef_$_type_150800,$tdef_Coq.Init.Decimal.uint,$tdef_Prop,$tdef_$_type_30735,$tdef_$_type_140785,$tdef_$_type_22967,$tdef_Coq.FSets.FMapPositive.PositiveMap.t,$tdef_$_type_54379,$tdef_$_type_26828,$tdef_$_type_1048,$tdef_$_type_10230,$tdef_$_type_208986,$tdef_$_type_10522,$tdef_$_type_28467,$tdef_$_type_2663,$tdef_$_type_141053,$tdef_$_type_140743,$tdef_$_type_56314,$tdef_$_type_41774,$tdef_$_type_206587,$tdef_$_type_4679,$tdef_Coq.Init.Datatypes.CompareSpecT,$tdef_Coq.micromega.RingMicromega.Op1,$tdef_$_type_2373,$tdef_$_type_31977,$tdef_$_type_206808,$tdef_$_type_155027,$tdef_$_type_2219,$tdef_Coq.setoid_ring.Field_theory.rsplit,$tdef_$_type_4236,$tdef_$_type_43087,$tdef_Coq.micromega.EnvRing.Pol,$tdef_$_type_29146,$tdef_$_type_1334,$tdef_$_type_141018,$tdef_$_type_149532,$tdef_$_type_4026,$tdef_$_type_10129,$tdef_$_type_3307,$tdef_$_type_494,$tdef_$_type_32037,$tdef_$_type_57076,$tdef_$_type_8071,$tdef_$_type_56929,$tdef_$_type_29345,$tdef_$_type_146385,$tdef_$_type_26851,$tdef_$_type_150757,$tdef_$_type_23084,$tdef_Coq.Bool.Bool.reflect,$tdef_$_type_141529,$tdef_$_type_681,$tdef_$_type_19454,$tdef_Coq.setoid_ring.Ring_polynom.Pol,$tdef_$_type_41971,$tdef_$_type_23923,$tdef_$_type_19425,$tdef_Color.graph,$tdef_$_type_26856,$tdef_$_type_1771,$tdef_$_type_22587,$tdef_$_type_1009,$tdef_$_type_145866,$tdef_$_type_9692,$tdef_$_type_41968,$tdef_$_type_140835,$tdef_$_type_149808,$tdef_$_type_42313,$tdef_$_type_702,$tdef_$_type_23974,$tdef_$_type_38854,$tdef_$_type_31669,$tdef_$_type_141195,$tdef_$_type_1046,$tdef_$_type_56111,$tdef_$_type_153862,$tdef_Coq.setoid_ring.Ring_polynom.PExpr,$tdef_Coq.micromega.RingMicromega.PolC,$tdef_$_type_29379,$tdef_$_type_31409,$tdef_$_type_10331,$tdef_$_type_4504,$tdef_$_type_10724,$tdef_$_type_208147,$tdef_$_type_576,$tdef_$_type_54250,$tdef_$_type_208002,$tdef_$_type_1058,$tdef_$_type_47282,$tdef_$_type_41945,$tdef_$_type_155307,$tdef_$_type_208937,$tdef_$_type_32042,$tdef_$_type_25474,$tdef_$_type_42451,$tdef_$_type_2277,$tdef_Type,$tdef_$_type_38898,$tdef_$_type_27433,$tdef_Coq.micromega.RingMicromega.NFormula,$tdef_$_type_149266,$tdef_$_type_2274,$tdef_$_type_143,$tdef_$_type_29181,$tdef_$_type_1779,$tdef_$_type_143734,$tdef_$_type_38819,$tdef_$_type_141875,$tdef_$_type_3645,$tdef_$_type_19458,$tdef_$_type_29153,$tdef_$_type_24853,$tdef_$_type_41266,$tdef_$_type_32678,$tdef_$_type_18976,$tdef_$_type_147700,$tdef_$_type_1006] % 23.70/23.20 =============================================================== % 23.70/23.20 % 23.70/23.20 Combined formula: 2867 axiom(s) => conjecture % 23.70/23.20 % 23.70/23.20 % Equality/functions detected -> nanoCoP oracle mode % 23.70/23.20 nanoCoP : % 23.70/23.20 % 16,904,434 inferences, 18.323 CPU in 18.325 seconds (100% CPU, 922559 Lips) % 23.70/23.20 % 23.70/23.20 % nanoCoP proof (equality/functions) % 23.70/23.20 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 23.70/23.20 % 23.70/23.20 % SZS output end Proof %------------------------------------------------------------------------------