%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SEV631+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 : n002.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:49 PM UTC 2026 % Result : Theorem 31.62s 31.47s % Output : Proof 31.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV631+1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.16/0.34 % Computer : n002.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 11 14:05:32 EDT 2026 % 0.16/0.34 % CPUTime : % 31.62/31.47 % SZS status Theorem % 31.62/31.47 % SZS output start Proof % 31.62/31.48 % 31.62/31.48 =============================================================== % 31.62/31.48 TPTP Problem: _HAMMER_GOAL (conjecture with 3117 axiom(s)) % 31.62/31.48 Axioms: [_HAMMER_COQ_TRUE,_HAMMER_COQ_FALSE,_HAMMER_COQ_TYPE_TYPE,$_case_Coq.Init.Datatypes.list$17865,$_case_Coq.Init.Datatypes.list$35694,$_case_Coq.Init.Datatypes.list$418,$_case_Coq.Init.Datatypes.list$46502,$_case_Coq.Init.Datatypes.list$505,$_case_Coq.Init.Datatypes.nat$120559,$_case_Coq.Init.Datatypes.nat$120581,$_case_Coq.Init.Datatypes.prod$33222,$_case_Coq.Init.Specif.sumbool$15756,$_case_Coq.Numbers.BinNums.Z$120576,$_case_Coq.Numbers.BinNums.Z$37861,$_case_Coq.setoid_ring.Ring_polynom.Pol$12167,$_case_Coq.setoid_ring.Ring_polynom.Pol$12766,$_case_ExtLib.Data.Member.member$17801,$_def_$_let_11_subst_l_24915,$_def_$_let_16_mkpow_28087,$_def_$_let_17_lnum_11934,$_def_$_let_17_mkopp_pow_28088,$_def_$_let_18_mkmult_pow_28089,$_def_$_let_20_lnum_12462,$_def_$_let_var_6_p_28807_28810,$_def_$_let_var_6_p_28809_28811,$_def_$_let_var_var_7_n_15725_15729_15738,$_def_Coq.Arith.PeanoNat.Nat.divide,$_def_Coq.Arith.PeanoNat.Nat.eqf,$_def_Coq.Bool.Bool.Is_true,$_def_Coq.FSets.FSetPositive.PositiveSet.Empty,$_def_Coq.FSets.FSetPositive.PositiveSet.In,$_def_Coq.FSets.FSetPositive.PositiveSet.add,$_def_Coq.FSets.FSetPositive.PositiveSet.elt,$_def_Coq.FSets.FSetPositive.PositiveSet.empty,$_def_Coq.FSets.FSetPositive.PositiveSet.mem,$_def_Coq.FSets.FSetPositive.PositiveSet.rev,$_def_Coq.FSets.FSetPositive.PositiveSet.rev_append,$_def_Coq.FSets.FSetPositive.PositiveSet.t,$_def_Coq.FSets.FSetPositive.PositiveSet.xelements,$_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.list_rec,$_def_Coq.Init.Datatypes.list_rect,$_def_Coq.Init.Datatypes.negb,$_def_Coq.Init.Datatypes.orb,$_def_Coq.Init.Datatypes.snd,$_def_Coq.Init.Datatypes.xorb,$_def_Coq.Init.Nat.add,$_def_Coq.Init.Nat.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.sub,$_def_Coq.Init.Peano.ge,$_def_Coq.Init.Peano.gt,$_def_Coq.Init.Peano.lt,$_def_Coq.Init.Specif.proj1_sig,$_def_Coq.Init.Specif.projT1,$_def_Coq.Init.Specif.projT2,$_def_Coq.Init.Specif.sumbool_rec,$_def_Coq.Lists.List.ForallPairs,$_def_Coq.Lists.List.In,$_def_Coq.Lists.List.combine,$_def_Coq.Lists.List.concat,$_def_Coq.Lists.List.count_occ,$_def_Coq.Lists.List.existsb,$_def_Coq.Lists.List.filter,$_def_Coq.Lists.List.find,$_def_Coq.Lists.List.firstn,$_def_Coq.Lists.List.flat_map,$_def_Coq.Lists.List.fold_left,$_def_Coq.Lists.List.fold_right,$_def_Coq.Lists.List.forallb,$_def_Coq.Lists.List.hd,$_def_Coq.Lists.List.hd_error,$_def_Coq.Lists.List.incl,$_def_Coq.Lists.List.last,$_def_Coq.Lists.List.lel,$_def_Coq.Lists.List.map,$_def_Coq.Lists.List.nodup,$_def_Coq.Lists.List.nth,$_def_Coq.Lists.List.nth_default,$_def_Coq.Lists.List.nth_error,$_def_Coq.Lists.List.nth_ok,$_def_Coq.Lists.List.partition,$_def_Coq.Lists.List.remove,$_def_Coq.Lists.List.removelast,$_def_Coq.Lists.List.repeat,$_def_Coq.Lists.List.rev,$_def_Coq.Lists.List.rev',$_def_Coq.Lists.List.rev_append,$_def_Coq.Lists.List.seq,$_def_Coq.Lists.List.skipn,$_def_Coq.Lists.List.split,$_def_Coq.Lists.List.tl,$_def_Coq.Lists.SetoidList.equivlistA,$_def_Coq.Lists.SetoidList.inclA,$_def_Coq.Lists.SetoidList.removeA,$_def_Coq.Lists.SetoidList.transpose,$_def_Coq.Lists.SetoidList.transpose2,$_def_Coq.Lists.SetoidList.transpose_restr,$_def_Coq.Lists.SetoidList.transpose_restr2,$_def_Coq.Logic.Decidable.decidable,$_def_Coq.Logic.EqdepFacts.Eq_dep_eq_on,$_def_Coq.Logic.EqdepFacts.Eq_rect_eq_on,$_def_Coq.Logic.EqdepFacts.Streicher_K_on_,$_def_Coq.Logic.EqdepFacts.UIP_on_,$_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.div_eucl,$_def_Coq.NArith.BinNatDef.N.eqb,$_def_Coq.NArith.BinNatDef.N.mul,$_def_Coq.NArith.BinNatDef.N.succ,$_def_Coq.NArith.BinNatDef.N.testbit,$_def_Coq.NArith.BinNatDef.N.to_nat,$_def_Coq.PArith.BinPos.Pos.lt,$_def_Coq.PArith.BinPosDef.Pos.add,$_def_Coq.PArith.BinPosDef.Pos.iter,$_def_Coq.PArith.BinPosDef.Pos.pred_double,$_def_Coq.PArith.BinPosDef.Pos.sub,$_def_Coq.PArith.BinPosDef.Pos.succ,$_def_Coq.QArith.QArith_base.Qdiv,$_def_Coq.QArith.QArith_base.Qeq,$_def_Coq.QArith.QArith_base.Qminus,$_def_Coq.QArith.QArith_base.Qmult,$_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.Sets.Relations_1.Transitive,$_def_Coq.Sorting.Sorted.StronglySorted_rect,$_def_Coq.Strings.String.list_ascii_of_string,$_def_Coq.Strings.String.string_of_list_ascii,$_def_Coq.Structures.OrderedTypeEx.N_as_OT.t,$_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.t,$_def_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$_def_Coq.Vectors.VectorDef.of_list,$_def_Coq.Vectors.VectorDef.to_list,$_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.gtb,$_def_Coq.ZArith.BinIntDef.Z.leb,$_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.pos_sub,$_def_Coq.ZArith.BinIntDef.Z.pow,$_def_Coq.ZArith.BinIntDef.Z.quotrem,$_def_Coq.ZArith.BinIntDef.Z.sub,$_def_Coq.ZArith.BinIntDef.Z.succ,$_def_Coq.ZArith.Zbool.Zeq_bool,$_def_Coq.ZArith.Zcomplements.Zlength,$_def_Coq.ZArith.Zcomplements.Zlength_aux,$_def_Coq.micromega.Env.Env,$_def_Coq.micromega.Refl.make_conj,$_def_Coq.micromega.Refl.make_impl,$_def_Coq.micromega.RingMicromega.NFormula,$_def_Coq.micromega.RingMicromega.PolC,$_def_Coq.micromega.RingMicromega.PolEnv,$_def_Coq.micromega.RingMicromega.ge_bool,$_def_Coq.micromega.Tauto.clause,$_def_Coq.micromega.Tauto.cnf,$_def_Coq.micromega.Tauto.cnf_checker,$_def_Coq.micromega.Tauto.collect_annot,$_def_Coq.micromega.Tauto.cons_id,$_def_Coq.micromega.Tauto.eval_clause,$_def_Coq.micromega.Tauto.eval_cnf,$_def_Coq.micromega.Tauto.eval_f,$_def_Coq.micromega.Tauto.eval_tt,$_def_Coq.micromega.ZMicromega.ZWitness,$_def_Coq.micromega.ZMicromega.Zunsat,$_def_Coq.micromega.ZMicromega.is_pol_Z0,$_def_Coq.micromega.ZMicromega.make_conj,$_def_Coq.micromega.ZMicromega.make_impl,$_def_Coq.micromega.ZMicromega.valid_cut_sign,$_def_Coq.setoid_ring.BinList.jump,$_def_Coq.setoid_ring.BinList.nth,$_def_Coq.setoid_ring.Field_theory.FEeval,$_def_Coq.setoid_ring.Field_theory.Fapp,$_def_Coq.setoid_ring.Field_theory.Fcons,$_def_Coq.setoid_ring.Field_theory.Fcons00,$_def_Coq.setoid_ring.Field_theory.Fcons2,$_def_Coq.setoid_ring.Field_theory.NPEequiv,$_def_Coq.setoid_ring.Field_theory.NPEopp,$_def_Coq.setoid_ring.Field_theory.PCond,$_def_Coq.setoid_ring.Field_theory.PExpr_eq,$_def_Coq.setoid_ring.Field_theory.absurd_PCond,$_def_Coq.setoid_ring.Field_theory.condition,$_def_Coq.setoid_ring.Field_theory.denum,$_def_Coq.setoid_ring.Field_theory.display_linear,$_def_Coq.setoid_ring.Field_theory.display_pow_linear,$_def_Coq.setoid_ring.Field_theory.num,$_def_Coq.setoid_ring.Field_theory.rsplit_common,$_def_Coq.setoid_ring.Field_theory.rsplit_left,$_def_Coq.setoid_ring.Field_theory.rsplit_right,$_def_Coq.setoid_ring.Field_theory.split,$_def_Coq.setoid_ring.InitialRing.Nopp,$_def_Coq.setoid_ring.InitialRing.Nsub,$_def_Coq.setoid_ring.InitialRing.Nwadd,$_def_Coq.setoid_ring.InitialRing.Nwcons,$_def_Coq.setoid_ring.InitialRing.Nword,$_def_Coq.setoid_ring.InitialRing.gen_phiN,$_def_Coq.setoid_ring.InitialRing.gen_phiNword,$_def_Coq.setoid_ring.InitialRing.gen_phiPOS,$_def_Coq.setoid_ring.InitialRing.gen_phiZ,$_def_Coq.setoid_ring.InitialRing.get_signZ,$_def_Coq.setoid_ring.InitialRing.triv_div,$_def_Coq.setoid_ring.Ring.bool_eq,$_def_Coq.setoid_ring.Ring_polynom.Mphi,$_def_Coq.setoid_ring.Ring_polynom.P0,$_def_Coq.setoid_ring.Ring_polynom.P1,$_def_Coq.setoid_ring.Ring_polynom.PEeval,$_def_Coq.setoid_ring.Ring_polynom.Peq,$_def_Coq.setoid_ring.Ring_polynom.Pequiv,$_def_Coq.setoid_ring.Ring_polynom.Pphi,$_def_Coq.setoid_ring.Ring_polynom.Pphi_pow,$_def_Coq.setoid_ring.Ring_polynom.add_pow_list,$_def_Coq.setoid_ring.Ring_polynom.interp_PElist,$_def_Coq.setoid_ring.Ring_polynom.mkPinj,$_def_Coq.setoid_ring.Ring_polynom.mkZmon,$_def_Coq.setoid_ring.Ring_polynom.mk_monpol_list,$_def_Coq.setoid_ring.Ring_polynom.mkmult_pow,$_def_Coq.setoid_ring.Ring_polynom.norm_subst,$_def_Coq.setoid_ring.Ring_polynom.r_list_pow,$_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,$_def_ExtLib.Data.Member.get_next,$_def_ExtLib.Data.Member.member_rec,$_def_ExtLib.Data.Member.member_rect,$_def_ExtLib.Data.Member.to_nat,$_def_ExtLib.Structures.Functor.ID,$_def_ExtLib.Tactics.Injection.result,$_def_HList.hlist.Injection_equiv_hlist_app,$_def_HList.hlist.Injection_equiv_hlist_cons,$_def_HList.hlist.hlist_app,$_def_HList.hlist.hlist_hd,$_def_HList.hlist.hlist_rec,$_def_HList.hlist.hlist_rect,$_def_HList.hlist.hlist_rev',$_def_HList.hlist.hlist_tl,$_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.RMicromega.C0$Coq.micromega.RMicromega.C1,$_discrim_Coq.micromega.RingMicromega.Equal$Coq.micromega.RingMicromega.NonEqual,$_discrim_Coq.micromega.RingMicromega.OpEq$Coq.micromega.RingMicromega.OpNEq,$_discrim_Coq.micromega.RingMicromega.PsatzIn$Coq.micromega.RingMicromega.PsatzSquare,$_discrim_Coq.micromega.Tauto.TT$Coq.micromega.Tauto.FF,$_discrim_Coq.micromega.ZMicromega.DoneProof$Coq.micromega.ZMicromega.RatProof,$_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,$_discrim_ExtLib.Data.Member.MZ$ExtLib.Data.Member.MN,$_discrim_HList.hlist.Hnil$HList.hlist.Hcons,$_fix_36692_v_CANONICAL_2,$_fix_37630_1_add_carry,$_fix_550_v_CANONICAL_1,$_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.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.RMicromega.CInv,$_inj_Coq.micromega.RMicromega.CMinus,$_inj_Coq.micromega.RMicromega.CMult,$_inj_Coq.micromega.RMicromega.COpp,$_inj_Coq.micromega.RMicromega.CPlus,$_inj_Coq.micromega.RMicromega.CPow,$_inj_Coq.micromega.RMicromega.CQ,$_inj_Coq.micromega.RMicromega.CZ,$_inj_Coq.micromega.RingMicromega.Build_Formula,$_inj_Coq.micromega.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.micromega.ZMicromega.CutProof,$_inj_Coq.micromega.ZMicromega.EnumProof,$_inj_Coq.micromega.ZMicromega.RatProof,$_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,$_inj_ExtLib.Core.RelDec.Build_RelDec,$_inj_ExtLib.Data.Member.MN,$_inj_ExtLib.Data.Member.MZ,$_inj_ExtLib.Tactics.Injection.Build_Injective,$_inj_HList.hlist.Hcons,$_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.Lists.List.Add,$_inversion_Coq.Lists.List.Exists,$_inversion_Coq.Lists.List.Forall,$_inversion_Coq.Lists.List.Forall2,$_inversion_Coq.Lists.List.ForallOrdPairs,$_inversion_Coq.Lists.List.NoDup,$_inversion_Coq.Lists.SetoidList.InA,$_inversion_Coq.Lists.SetoidList.NoDupA,$_inversion_Coq.Lists.SetoidList.eqlistA,$_inversion_Coq.Logic.EqdepFacts.eq_dep,$_inversion_Coq.Logic.EqdepFacts.eq_dep1,$_inversion_Coq.Logic.JMeq.JMeq,$_inversion_Coq.Numbers.BinNums.N,$_inversion_Coq.Numbers.BinNums.Z,$_inversion_Coq.Numbers.BinNums.positive,$_inversion_Coq.PArith.BinPosDef.Pos.mask,$_inversion_Coq.QArith.QArith_base.Q,$_inversion_Coq.Reals.Rfunctions.Z_spec,$_inversion_Coq.Relations.Relation_Operators.Desc,$_inversion_Coq.Relations.Relation_Operators.Ltl,$_inversion_Coq.Relations.Relation_Operators.clos_refl,$_inversion_Coq.Sorting.Sorted.HdRel,$_inversion_Coq.Sorting.Sorted.LocallySorted,$_inversion_Coq.Sorting.Sorted.Sorted,$_inversion_Coq.Sorting.Sorted.StronglySorted,$_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.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.RMicromega.Rcst,$_inversion_Coq.micromega.RingMicromega.Formula,$_inversion_Coq.micromega.RingMicromega.Op1,$_inversion_Coq.micromega.RingMicromega.Op2,$_inversion_Coq.micromega.RingMicromega.Psatz,$_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.ZArithProof,$_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,$_inversion_ExtLib.Core.RelDec.RelDec,$_inversion_ExtLib.Data.Member.member,$_inversion_ExtLib.Tactics.Injection.Injective,$_inversion_HList.hlist.equiv_hlist,$_inversion_HList.hlist.hlist,$_lam_126658,$_lam_15512,$_lam_15516,$_lam_16626,$_lam_16646,$_lam_16675,$_lam_17884,$_lam_17912,$_lam_2042,$_lam_2046,$_lam_24987,$_lam_34898,$_lam_34917,$_lam_34982,$_lam_35023,$_lam_38194,$_lam_38202,$_lam_46511,$_lam_46514,$_lam_47639,$_lam_47646,$_lam_48310,$_prop_116340,$_prop_116341,$_prop_116342,$_prop_116343,$_prop_116344,$_prop_116345,$_prop_116346,$_prop_122450,$_prop_126634,$_prop_126659,$_prop_126660,$_prop_126684,$_prop_15517,$_prop_15623,$_prop_15624,$_prop_15659,$_prop_15696,$_prop_15697,$_prop_15698,$_prop_15699,$_prop_15768,$_prop_15769,$_prop_15770,$_prop_15771,$_prop_16607,$_prop_16608,$_prop_16616,$_prop_16617,$_prop_16914,$_prop_16926,$_prop_34458,$_prop_34459,$_prop_34460,$_prop_34493,$_prop_37864,$_prop_37889,$_prop_37890,$_prop_45254,$_prop_46976,$_prop_46989,$_type_109,$_type_11157,$_type_11205,$_type_11216,$_type_11236,$_type_11239,$_type_11311,$_type_11368,$_type_113947,$_type_114118,$_type_114199,$_type_114203,$_type_116455,$_type_116538,$_type_118289,$_type_118488,$_type_118673,$_type_120240,$_type_120259,$_type_120279,$_type_120501,$_type_120510,$_type_120588,$_type_121139,$_type_121264,$_type_121389,$_type_121514,$_type_121639,$_type_1217,$_type_121764,$_type_121875,$_type_122416,$_type_122667,$_type_122692,$_type_12420,$_type_12444,$_type_126485,$_type_126682,$_type_126706,$_type_126742,$_type_12789,$_type_13125,$_type_13160,$_type_13677,$_type_13682,$_type_13751,$_type_13781,$_type_13903,$_type_14698,$_type_15282,$_type_15293,$_type_15309,$_type_15311,$_type_15345,$_type_15387,$_type_15433,$_type_15450,$_type_15463,$_type_15477,$_type_15488,$_type_15497,$_type_15505,$_type_15621,$_type_15649,$_type_15657,$_type_15670,$_type_15709,$_type_15781,$_type_159676,$_type_159686,$_type_159798,$_type_16605,$_type_16614,$_type_16632,$_type_16735,$_type_16770,$_type_16820,$_type_16933,$_type_16977,$_type_17166,$_type_17185,$_type_17419,$_type_17451,$_type_17485,$_type_17521,$_type_17550,$_type_17562,$_type_17592,$_type_17645,$_type_17652,$_type_17661,$_type_17685,$_type_17692,$_type_17771,$_type_18076,$_type_18130,$_type_18598,$_type_18699,$_type_18800,$_type_18890,$_type_18991,$_type_1905,$_type_1907,$_type_19092,$_type_1912,$_type_1914,$_type_19193,$_type_1926,$_type_19434,$_type_19437,$_type_19443,$_type_1951,$_type_1954,$_type_1966,$_type_19666,$_type_19669,$_type_19675,$_type_19693,$_type_19752,$_type_1976,$_type_19798,$_type_2,$_type_2001,$_type_2023,$_type_2035,$_type_20451,$_type_2055,$_type_2071,$_type_20807,$_type_20812,$_type_20820,$_type_20962,$_type_2118,$_type_2125,$_type_2143,$_type_2153,$_type_2170,$_type_21736,$_type_2174,$_type_2177,$_type_2194,$_type_220,$_type_2211,$_type_2215,$_type_2218,$_type_2235,$_type_2286,$_type_23083,$_type_2310,$_type_23156,$_type_23220,$_type_2357,$_type_2361,$_type_23647,$_type_2379,$_type_2401,$_type_24174,$_type_24177,$_type_24180,$_type_24185,$_type_24194,$_type_24199,$_type_2434,$_type_2445,$_type_2511,$_type_25119,$_type_2522,$_type_2533,$_type_25373,$_type_2554,$_type_25658,$_type_2628,$_type_26565,$_type_2663,$_type_2671,$_type_2684,$_type_2686,$_type_2699,$_type_27980,$_type_28,$_type_28367,$_type_28821,$_type_28842,$_type_29096,$_type_29159,$_type_29222,$_type_29276,$_type_29339,$_type_2947,$_type_2952,$_type_29553,$_type_29576,$_type_29599,$_type_2961,$_type_29622,$_type_29640,$_type_29666,$_type_2968,$_type_29684,$_type_2973,$_type_29817,$_type_2982,$_type_29847,$_type_29871,$_type_29901,$_type_29931,$_type_29955,$_type_29988,$_type_30012,$_type_30039,$_type_30492,$_type_3064,$_type_3068,$_type_30705,$_type_30918,$_type_3103,$_type_3110,$_type_31113,$_type_31326,$_type_3139,$_type_3146,$_type_3153,$_type_31539,$_type_3166,$_type_31752,$_type_3185,$_type_31965,$_type_32160,$_type_3218,$_type_32373,$_type_32568,$_type_3259,$_type_3262,$_type_32784,$_type_32803,$_type_32817,$_type_3288,$_type_32967,$_type_33017,$_type_33067,$_type_33109,$_type_33159,$_type_33241,$_type_33364,$_type_33408,$_type_33444,$_type_33488,$_type_33500,$_type_33536,$_type_33708,$_type_33790,$_type_33834,$_type_34438,$_type_34447,$_type_34456,$_type_34479,$_type_34491,$_type_34711,$_type_34826,$_type_34861,$_type_34907,$_type_35080,$_type_35115,$_type_35187,$_type_35193,$_type_35210,$_type_35216,$_type_35233,$_type_35239,$_type_35252,$_type_35275,$_type_35280,$_type_35306,$_type_35310,$_type_35317,$_type_35324,$_type_35336,$_type_35359,$_type_35364,$_type_35376,$_type_35414,$_type_35420,$_type_35433,$_type_35588,$_type_36141,$_type_36170,$_type_36199,$_type_36319,$_type_36343,$_type_36598,$_type_36615,$_type_36623,$_type_36633,$_type_36706,$_type_36729,$_type_37027,$_type_37032,$_type_37581,$_type_37593,$_type_37596,$_type_37617,$_type_37624,$_type_37627,$_type_37660,$_type_37700,$_type_37702,$_type_37717,$_type_37722,$_type_37724,$_type_37742,$_type_37757,$_type_37761,$_type_37782,$_type_37785,$_type_37852,$_type_37914,$_type_38089,$_type_38092,$_type_38095,$_type_38100,$_type_38109,$_type_38118,$_type_38174,$_type_38179,$_type_38186,$_type_38205,$_type_38243,$_type_38366,$_type_38450,$_type_38465,$_type_3876,$_type_39000,$_type_39346,$_type_3945,$_type_39692,$_type_3988,$_type_40015,$_type_40361,$_type_4063,$_type_40707,$_type_4104,$_type_41053,$_type_4114,$_type_4129,$_type_41399,$_type_4143,$_type_41745,$_type_42068,$_type_42414,$_type_42760,$_type_43083,$_type_43406,$_type_4367,$_type_43752,$_type_44,$_type_44204,$_type_4436,$_type_45001,$_type_45156,$_type_45164,$_type_45172,$_type_45240,$_type_45243,$_type_45258,$_type_45279,$_type_45285,$_type_45330,$_type_45384,$_type_45389,$_type_46391,$_type_46401,$_type_46406,$_type_46415,$_type_46417,$_type_46443,$_type_46451,$_type_46459,$_type_46478,$_type_46480,$_type_46488,$_type_46490,$_type_46515,$_type_46531,$_type_46547,$_type_46580,$_type_46583,$_type_46600,$_type_46603,$_type_46627,$_type_46666,$_type_46686,$_type_46974,$_type_46987,$_type_47653,$_type_47675,$_type_48237,$_type_48333,$_type_4998,$_type_5009,$_type_5011,$_type_5024,$_type_5034,$_type_5063,$_type_5068,$_type_5080,$_type_5092,$_type_5123,$_type_5381,$_type_64,$_type_646,$_type_6868,$_type_6875,$_type_69,$_type_7071,$_type_7164,$_type_72,$_type_724,$_type_7257,$_type_7339,$_type_7432,$_type_7514,$_type_7607,$_type_7748,$_type_7767,$_type_7969,$_type_8672,$_type_87,$_type_9,$_type_9700,$_type_99,$_typeof_Coq.Arith.PeanoNat.Nat.divide,$_typeof_Coq.Arith.PeanoNat.Nat.eqf,$_typeof_Coq.Bool.Bool.Is_true,$_typeof_Coq.Bool.Bool.reflect,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.In,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Leaf,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Node,$_typeof_Coq.FSets.FSetPositive.PositiveSet.add,$_typeof_Coq.FSets.FSetPositive.PositiveSet.elt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.mem,$_typeof_Coq.FSets.FSetPositive.PositiveSet.rev,$_typeof_Coq.FSets.FSetPositive.PositiveSet.rev_append,$_typeof_Coq.FSets.FSetPositive.PositiveSet.t,$_typeof_Coq.FSets.FSetPositive.PositiveSet.tree,$_typeof_Coq.FSets.FSetPositive.PositiveSet.xelements,$_typeof_Coq.Init.Byte.byte,$_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.list_rec,$_typeof_Coq.Init.Datatypes.list_rect,$_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.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.sub,$_typeof_Coq.Init.Peano.ge,$_typeof_Coq.Init.Peano.gt,$_typeof_Coq.Init.Peano.lt,$_typeof_Coq.Init.Specif.exist,$_typeof_Coq.Init.Specif.existT,$_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.sumbool_rec,$_typeof_Coq.Init.Specif.sumor,$_typeof_Coq.Lists.List.ForallPairs,$_typeof_Coq.Lists.List.Forall_rect,$_typeof_Coq.Lists.List.In,$_typeof_Coq.Lists.List.combine,$_typeof_Coq.Lists.List.concat,$_typeof_Coq.Lists.List.count_occ,$_typeof_Coq.Lists.List.destruct_list,$_typeof_Coq.Lists.List.exists_last,$_typeof_Coq.Lists.List.existsb,$_typeof_Coq.Lists.List.filter,$_typeof_Coq.Lists.List.find,$_typeof_Coq.Lists.List.firstn,$_typeof_Coq.Lists.List.flat_map,$_typeof_Coq.Lists.List.fold_left,$_typeof_Coq.Lists.List.fold_right,$_typeof_Coq.Lists.List.forallb,$_typeof_Coq.Lists.List.hd,$_typeof_Coq.Lists.List.hd_error,$_typeof_Coq.Lists.List.incl,$_typeof_Coq.Lists.List.last,$_typeof_Coq.Lists.List.lel,$_typeof_Coq.Lists.List.map,$_typeof_Coq.Lists.List.nodup,$_typeof_Coq.Lists.List.nth,$_typeof_Coq.Lists.List.nth_default,$_typeof_Coq.Lists.List.nth_error,$_typeof_Coq.Lists.List.nth_in_or_default,$_typeof_Coq.Lists.List.nth_ok,$_typeof_Coq.Lists.List.partition,$_typeof_Coq.Lists.List.remove,$_typeof_Coq.Lists.List.removelast,$_typeof_Coq.Lists.List.repeat,$_typeof_Coq.Lists.List.rev,$_typeof_Coq.Lists.List.rev',$_typeof_Coq.Lists.List.rev_append,$_typeof_Coq.Lists.List.seq,$_typeof_Coq.Lists.List.skipn,$_typeof_Coq.Lists.List.split,$_typeof_Coq.Lists.List.tl,$_typeof_Coq.Lists.SetoidList.equivlistA,$_typeof_Coq.Lists.SetoidList.inclA,$_typeof_Coq.Lists.SetoidList.removeA,$_typeof_Coq.Lists.SetoidList.transpose,$_typeof_Coq.Lists.SetoidList.transpose2,$_typeof_Coq.Lists.SetoidList.transpose_restr,$_typeof_Coq.Lists.SetoidList.transpose_restr2,$_typeof_Coq.Logic.Decidable.decidable,$_typeof_Coq.Logic.EqdepFacts.Eq_dep_eq_on,$_typeof_Coq.Logic.EqdepFacts.Eq_rect_eq_on,$_typeof_Coq.Logic.EqdepFacts.Streicher_K_on_,$_typeof_Coq.Logic.EqdepFacts.UIP_on_,$_typeof_Coq.Logic.EqdepFacts.internal_eq_rew_r_dep,$_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.div_eucl,$_typeof_Coq.NArith.BinNatDef.N.eqb,$_typeof_Coq.NArith.BinNatDef.N.mul,$_typeof_Coq.NArith.BinNatDef.N.succ,$_typeof_Coq.NArith.BinNatDef.N.testbit,$_typeof_Coq.NArith.BinNatDef.N.to_nat,$_typeof_Coq.Numbers.BinNums.N,$_typeof_Coq.Numbers.BinNums.N0,$_typeof_Coq.Numbers.BinNums.Npos,$_typeof_Coq.Numbers.BinNums.Z,$_typeof_Coq.Numbers.BinNums.Z0,$_typeof_Coq.Numbers.BinNums.Zneg,$_typeof_Coq.Numbers.BinNums.Zpos,$_typeof_Coq.Numbers.BinNums.positive,$_typeof_Coq.Numbers.BinNums.xH,$_typeof_Coq.Numbers.BinNums.xI,$_typeof_Coq.Numbers.BinNums.xO,$_typeof_Coq.PArith.BinPos.Pos.lt,$_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.iter,$_typeof_Coq.PArith.BinPosDef.Pos.mask,$_typeof_Coq.PArith.BinPosDef.Pos.pred_double,$_typeof_Coq.PArith.BinPosDef.Pos.sub,$_typeof_Coq.PArith.BinPosDef.Pos.succ,$_typeof_Coq.QArith.QArith_base.Q,$_typeof_Coq.QArith.QArith_base.Qdiv,$_typeof_Coq.QArith.QArith_base.Qeq,$_typeof_Coq.QArith.QArith_base.Qmake,$_typeof_Coq.QArith.QArith_base.Qminus,$_typeof_Coq.QArith.QArith_base.Qmult,$_typeof_Coq.Reals.Rdefinitions.IZR,$_typeof_Coq.Reals.Rdefinitions.R,$_typeof_Coq.Reals.Rdefinitions.R0,$_typeof_Coq.Reals.Rdefinitions.R1,$_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.Rfunctions.Z_spec,$_typeof_Coq.Reals.Rpow_def.pow,$_typeof_Coq.Relations.Relation_Definitions.relation,$_typeof_Coq.Setoids.Setoid.Setoid_Theory,$_typeof_Coq.Sets.Relations_1.Transitive,$_typeof_Coq.Sorting.Sorted.Sorted_rect,$_typeof_Coq.Sorting.Sorted.StronglySorted_rec,$_typeof_Coq.Sorting.Sorted.StronglySorted_rect,$_typeof_Coq.Strings.Ascii.ascii,$_typeof_Coq.Strings.String.EmptyString,$_typeof_Coq.Strings.String.String,$_typeof_Coq.Strings.String.list_ascii_of_string,$_typeof_Coq.Strings.String.string,$_typeof_Coq.Strings.String.string_of_list_ascii,$_typeof_Coq.Structures.OrderedType.Compare,$_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$_typeof_Coq.Structures.OrdersTac.OEQ,$_typeof_Coq.Structures.OrdersTac.ord,$_typeof_Coq.Vectors.Fin.t,$_typeof_Coq.Vectors.VectorDef.cons,$_typeof_Coq.Vectors.VectorDef.nil,$_typeof_Coq.Vectors.VectorDef.of_list,$_typeof_Coq.Vectors.VectorDef.t,$_typeof_Coq.Vectors.VectorDef.to_list,$_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.gtb,$_typeof_Coq.ZArith.BinIntDef.Z.leb,$_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.pos_sub,$_typeof_Coq.ZArith.BinIntDef.Z.pow,$_typeof_Coq.ZArith.BinIntDef.Z.quotrem,$_typeof_Coq.ZArith.BinIntDef.Z.sub,$_typeof_Coq.ZArith.BinIntDef.Z.succ,$_typeof_Coq.ZArith.Zbool.Zeq_bool,$_typeof_Coq.ZArith.Zcomplements.Zlength,$_typeof_Coq.ZArith.Zcomplements.Zlength_aux,$_typeof_Coq.ZArith.Znumtheory.Euclid,$_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs,$_typeof_Coq.micromega.Env.Env,$_typeof_Coq.micromega.EnvRing.Mon,$_typeof_Coq.micromega.EnvRing.PExpr,$_typeof_Coq.micromega.EnvRing.Pc,$_typeof_Coq.micromega.EnvRing.Pol,$_typeof_Coq.micromega.RMicromega.Rcst,$_typeof_Coq.micromega.Refl.make_conj,$_typeof_Coq.micromega.Refl.make_impl,$_typeof_Coq.micromega.RingMicromega.Equal,$_typeof_Coq.micromega.RingMicromega.Formula,$_typeof_Coq.micromega.RingMicromega.NFormula,$_typeof_Coq.micromega.RingMicromega.NonEqual,$_typeof_Coq.micromega.RingMicromega.NonStrict,$_typeof_Coq.micromega.RingMicromega.Op1,$_typeof_Coq.micromega.RingMicromega.Op2,$_typeof_Coq.micromega.RingMicromega.PolC,$_typeof_Coq.micromega.RingMicromega.PolEnv,$_typeof_Coq.micromega.RingMicromega.Psatz,$_typeof_Coq.micromega.RingMicromega.Strict,$_typeof_Coq.micromega.RingMicromega.ge_bool,$_typeof_Coq.micromega.Tauto.GFormula,$_typeof_Coq.micromega.Tauto.clause,$_typeof_Coq.micromega.Tauto.cnf,$_typeof_Coq.micromega.Tauto.cnf_checker,$_typeof_Coq.micromega.Tauto.collect_annot,$_typeof_Coq.micromega.Tauto.cons_id,$_typeof_Coq.micromega.Tauto.eval_clause,$_typeof_Coq.micromega.Tauto.eval_cnf,$_typeof_Coq.micromega.Tauto.eval_f,$_typeof_Coq.micromega.Tauto.eval_tt,$_typeof_Coq.micromega.ZMicromega.DoneProof,$_typeof_Coq.micromega.ZMicromega.ZArithProof,$_typeof_Coq.micromega.ZMicromega.ZWitness,$_typeof_Coq.micromega.ZMicromega.Zunsat,$_typeof_Coq.micromega.ZMicromega.is_pol_Z0,$_typeof_Coq.micromega.ZMicromega.make_conj,$_typeof_Coq.micromega.ZMicromega.make_impl,$_typeof_Coq.micromega.ZMicromega.valid_cut_sign,$_typeof_Coq.setoid_ring.BinList.jump,$_typeof_Coq.setoid_ring.BinList.nth,$_typeof_Coq.setoid_ring.Field_theory.FEI,$_typeof_Coq.setoid_ring.Field_theory.FEO,$_typeof_Coq.setoid_ring.Field_theory.FEX,$_typeof_Coq.setoid_ring.Field_theory.FEadd,$_typeof_Coq.setoid_ring.Field_theory.FEc,$_typeof_Coq.setoid_ring.Field_theory.FEdiv,$_typeof_Coq.setoid_ring.Field_theory.FEeval,$_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.FEpow,$_typeof_Coq.setoid_ring.Field_theory.FEsub,$_typeof_Coq.setoid_ring.Field_theory.FExpr,$_typeof_Coq.setoid_ring.Field_theory.Fapp,$_typeof_Coq.setoid_ring.Field_theory.Fcons,$_typeof_Coq.setoid_ring.Field_theory.Fcons00,$_typeof_Coq.setoid_ring.Field_theory.Fcons2,$_typeof_Coq.setoid_ring.Field_theory.NPEequiv,$_typeof_Coq.setoid_ring.Field_theory.NPEopp,$_typeof_Coq.setoid_ring.Field_theory.PCond,$_typeof_Coq.setoid_ring.Field_theory.PExpr_eq,$_typeof_Coq.setoid_ring.Field_theory.absurd_PCond,$_typeof_Coq.setoid_ring.Field_theory.ceqb_spec',$_typeof_Coq.setoid_ring.Field_theory.condition,$_typeof_Coq.setoid_ring.Field_theory.denum,$_typeof_Coq.setoid_ring.Field_theory.display_linear,$_typeof_Coq.setoid_ring.Field_theory.display_pow_linear,$_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_common,$_typeof_Coq.setoid_ring.Field_theory.rsplit_left,$_typeof_Coq.setoid_ring.Field_theory.rsplit_right,$_typeof_Coq.setoid_ring.Field_theory.split,$_typeof_Coq.setoid_ring.InitialRing.Nopp,$_typeof_Coq.setoid_ring.InitialRing.Nsub,$_typeof_Coq.setoid_ring.InitialRing.Nwadd,$_typeof_Coq.setoid_ring.InitialRing.Nwcons,$_typeof_Coq.setoid_ring.InitialRing.Nword,$_typeof_Coq.setoid_ring.InitialRing.gen_phiN,$_typeof_Coq.setoid_ring.InitialRing.gen_phiNword,$_typeof_Coq.setoid_ring.InitialRing.gen_phiPOS,$_typeof_Coq.setoid_ring.InitialRing.gen_phiZ,$_typeof_Coq.setoid_ring.InitialRing.get_signZ,$_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.Mphi,$_typeof_Coq.setoid_ring.Ring_polynom.P0,$_typeof_Coq.setoid_ring.Ring_polynom.P1,$_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.Pequiv,$_typeof_Coq.setoid_ring.Ring_polynom.Pinj,$_typeof_Coq.setoid_ring.Ring_polynom.Pol,$_typeof_Coq.setoid_ring.Ring_polynom.Pphi,$_typeof_Coq.setoid_ring.Ring_polynom.Pphi_pow,$_typeof_Coq.setoid_ring.Ring_polynom.add_pow_list,$_typeof_Coq.setoid_ring.Ring_polynom.interp_PElist,$_typeof_Coq.setoid_ring.Ring_polynom.mkPinj,$_typeof_Coq.setoid_ring.Ring_polynom.mkZmon,$_typeof_Coq.setoid_ring.Ring_polynom.mk_monpol_list,$_typeof_Coq.setoid_ring.Ring_polynom.mkmult_pow,$_typeof_Coq.setoid_ring.Ring_polynom.mon0,$_typeof_Coq.setoid_ring.Ring_polynom.norm_subst,$_typeof_Coq.setoid_ring.Ring_polynom.r_list_pow,$_typeof_Coq.setoid_ring.Ring_polynom.vmon,$_typeof_Coq.setoid_ring.Ring_polynom.zmon,$_typeof_Coq.setoid_ring.Ring_tac.ring_subst_niter,$_typeof_Coq.setoid_ring.Ring_theory.IDphi,$_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,$_typeof_ExtLib.Core.RelDec.RelDec,$_typeof_ExtLib.Data.Member.MN,$_typeof_ExtLib.Data.Member.MZ,$_typeof_ExtLib.Data.Member.get_next,$_typeof_ExtLib.Data.Member.member,$_typeof_ExtLib.Data.Member.member_rec,$_typeof_ExtLib.Data.Member.member_rect,$_typeof_ExtLib.Data.Member.to_nat,$_typeof_ExtLib.Structures.Functor.ID,$_typeof_ExtLib.Tactics.Injection.Build_Injective,$_typeof_ExtLib.Tactics.Injection.Injective,$_typeof_ExtLib.Tactics.Injection.result,$_typeof_F,$_typeof_HList.hlist.Hcons,$_typeof_HList.hlist.Hnil,$_typeof_HList.hlist.Injection_equiv_hlist_app,$_typeof_HList.hlist.Injection_equiv_hlist_cons,$_typeof_HList.hlist.hlist,$_typeof_HList.hlist.hlist_app,$_typeof_HList.hlist.hlist_hd,$_typeof_HList.hlist.hlist_rec,$_typeof_HList.hlist.hlist_rect,$_typeof_HList.hlist.hlist_rev,$_typeof_HList.hlist.hlist_rev',$_typeof_HList.hlist.hlist_tl,$_typeof_iT,Coq.Arith.Gt.gt_S_le,Coq.Arith.Gt.gt_Sn_O,Coq.Arith.Gt.gt_irrefl,Coq.Arith.Gt.gt_le_S,Coq.Arith.Gt.gt_not_le,Coq.Arith.Le.le_S_n,Coq.Arith.Le.le_n_0_eq,Coq.Arith.Le.le_n_S,Coq.Arith.Lt.le_lt_n_Sm,Coq.Arith.Lt.lt_S_n,Coq.Arith.Lt.lt_le_S,Coq.Arith.Lt.lt_n_S,Coq.Arith.Minus.minus_diag_reverse,Coq.Arith.Minus.minus_n_O,Coq.Arith.Minus.minus_plus,Coq.Arith.Minus.minus_plus_simpl_l_reverse,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.lt_irrefl,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.neq_eq,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_neq_eq,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_neq,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_refl,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_sym,Coq.Arith.PeanoNat.Nat.Private_Tac.le_antisym,Coq.Arith.PeanoNat.Nat.Private_Tac.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_comm,Coq.Arith.PeanoNat.Nat.eq_equiv,Coq.Arith.PeanoNat.Nat.eq_le_incl,Coq.Arith.PeanoNat.Nat.eq_stepl,Coq.Arith.PeanoNat.Nat.le_0_l,Coq.Arith.PeanoNat.Nat.le_0_r,Coq.Arith.PeanoNat.Nat.le_antisymm,Coq.Arith.PeanoNat.Nat.le_ge_cases,Coq.Arith.PeanoNat.Nat.le_gt_cases,Coq.Arith.PeanoNat.Nat.le_trans,Coq.Arith.PeanoNat.Nat.lt_0_succ,Coq.Arith.PeanoNat.Nat.lt_le_incl,Coq.Arith.PeanoNat.Nat.lt_trichotomy,Coq.Arith.PeanoNat.Nat.neq_sym,Coq.Arith.PeanoNat.Nat.nle_succ_0,Coq.Arith.PeanoNat.Nat.nlt_ge,Coq.Arith.PeanoNat.Nat.sub_0_le,Coq.Arith.PeanoNat.Nat.sub_0_r,Coq.Arith.PeanoNat.Nat.sub_add,Coq.Arith.PeanoNat.Nat.sub_diag,Coq.Arith.PeanoNat.Nat.sub_wd,Coq.Arith.PeanoNat.Nat.succ_inj,Coq.Arith.Plus.le_plus_l,Coq.Arith.Plus.le_plus_r,Coq.Bool.Bool.absurd_eq_true,Coq.Bool.Bool.eq_true_iff_eq,Coq.Bool.Bool.orb_false_elim,Coq.Bool.Bool.orb_prop,Coq.Bool.Bool.orb_true_intro,Coq.Bool.Bool.trans_eq_bool,Coq.FSets.FSetPositive.PositiveSet.tree_ind,Coq.Init.Datatypes.andb_prop,Coq.Init.Datatypes.list_ind,Coq.Init.Datatypes.list_sind,Coq.Init.Datatypes.nat_ind,Coq.Init.Peano.eq_add_S,Coq.Init.Peano.f_equal_nat,Coq.Init.Peano.le_S,Coq.Init.Peano.le_S_n,Coq.Init.Peano.le_n,Coq.Init.Peano.le_n_S,Coq.Init.Peano.plus_n_O,Coq.Init.Peano.plus_n_Sm,Coq.Lists.List.Add_app,Coq.Lists.List.Add_cons,Coq.Lists.List.Add_head,Coq.Lists.List.Add_in,Coq.Lists.List.Add_ind,Coq.Lists.List.Add_inv,Coq.Lists.List.Add_length,Coq.Lists.List.Add_sind,Coq.Lists.List.Add_split,Coq.Lists.List.Exists_cons,Coq.Lists.List.Exists_cons_hd,Coq.Lists.List.Exists_cons_tl,Coq.Lists.List.Exists_dec_subproof,Coq.Lists.List.Exists_dec_subproof0,Coq.Lists.List.Exists_exists,Coq.Lists.List.Exists_impl,Coq.Lists.List.Exists_ind,Coq.Lists.List.Exists_sind,Coq.Lists.List.FOP_cons,Coq.Lists.List.Forall2_app,Coq.Lists.List.Forall2_app_inv_l,Coq.Lists.List.Forall2_app_inv_r,Coq.Lists.List.Forall2_cons,Coq.Lists.List.Forall2_ind,Coq.Lists.List.Forall2_nil,Coq.Lists.List.Forall2_sind,Coq.Lists.List.ForallOrdPairs_ForallPairs,Coq.Lists.List.ForallOrdPairs_In,Coq.Lists.List.ForallOrdPairs_ind,Coq.Lists.List.ForallOrdPairs_sind,Coq.Lists.List.ForallPairs_ForallOrdPairs,Coq.Lists.List.Forall_cons,Coq.Lists.List.Forall_dec_subproof,Coq.Lists.List.Forall_dec_subproof0,Coq.Lists.List.Forall_forall,Coq.Lists.List.Forall_impl,Coq.Lists.List.Forall_ind,Coq.Lists.List.Forall_inv,Coq.Lists.List.Forall_inv_tail,Coq.Lists.List.Forall_nil,Coq.Lists.List.Forall_sind,Coq.Lists.List.In_nth,Coq.Lists.List.In_nth_error,Coq.Lists.List.NoDup_Add,Coq.Lists.List.NoDup_cons,Coq.Lists.List.NoDup_cons_iff,Coq.Lists.List.NoDup_incl_length,Coq.Lists.List.NoDup_ind,Coq.Lists.List.NoDup_map_inv,Coq.Lists.List.NoDup_nil,Coq.Lists.List.NoDup_nodup,Coq.Lists.List.NoDup_nth,Coq.Lists.List.NoDup_nth_error,Coq.Lists.List.NoDup_remove,Coq.Lists.List.NoDup_remove_1,Coq.Lists.List.NoDup_remove_2,Coq.Lists.List.NoDup_sind,Coq.Lists.List.app_assoc,Coq.Lists.List.app_assoc_reverse,Coq.Lists.List.app_comm_cons,Coq.Lists.List.app_cons_not_nil,Coq.Lists.List.app_eq_nil,Coq.Lists.List.app_eq_unit,Coq.Lists.List.app_inj_tail,Coq.Lists.List.app_inv_head,Coq.Lists.List.app_inv_tail,Coq.Lists.List.app_length,Coq.Lists.List.app_nil_end,Coq.Lists.List.app_nil_l,Coq.Lists.List.app_nil_r,Coq.Lists.List.app_nth1,Coq.Lists.List.app_removelast_last,Coq.Lists.List.concat_cons,Coq.Lists.List.count_occ_cons_eq,Coq.Lists.List.count_occ_cons_neq,Coq.Lists.List.count_occ_inv_nil,Coq.Lists.List.count_occ_map,Coq.Lists.List.count_occ_not_In,Coq.Lists.List.existsb_exists,Coq.Lists.List.existsb_nth,Coq.Lists.List.ext_in_map,Coq.Lists.List.filter_In,Coq.Lists.List.find_none,Coq.Lists.List.find_some,Coq.Lists.List.firstn_O,Coq.Lists.List.firstn_all,Coq.Lists.List.firstn_all2,Coq.Lists.List.firstn_cons,Coq.Lists.List.firstn_firstn,Coq.Lists.List.firstn_le_length,Coq.Lists.List.firstn_length_le,Coq.Lists.List.firstn_skipn,Coq.Lists.List.fold_left_app,Coq.Lists.List.fold_left_rev_right,Coq.Lists.List.fold_right_app,Coq.Lists.List.fold_symmetric,Coq.Lists.List.forallb_forall,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_iff,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_map,Coq.Lists.List.in_map_iff,Coq.Lists.List.in_nil,Coq.Lists.List.in_or_app,Coq.Lists.List.in_rev,Coq.Lists.List.in_split,Coq.Lists.List.incl_Add_inv,Coq.Lists.List.incl_app,Coq.Lists.List.incl_appl,Coq.Lists.List.incl_appr,Coq.Lists.List.incl_cons,Coq.Lists.List.incl_refl,Coq.Lists.List.incl_tl,Coq.Lists.List.incl_tran,Coq.Lists.List.lel_cons,Coq.Lists.List.lel_cons_cons,Coq.Lists.List.lel_nil,Coq.Lists.List.lel_refl,Coq.Lists.List.lel_tail,Coq.Lists.List.lel_trans,Coq.Lists.List.length_zero_iff_nil,Coq.Lists.List.map_app,Coq.Lists.List.map_cons,Coq.Lists.List.map_eq_nil,Coq.Lists.List.map_ext,Coq.Lists.List.map_ext_in,Coq.Lists.List.map_ext_in_iff,Coq.Lists.List.map_id,Coq.Lists.List.map_length,Coq.Lists.List.map_map,Coq.Lists.List.map_nth,Coq.Lists.List.nil_cons,Coq.Lists.List.nodup_In,Coq.Lists.List.nodup_inv,Coq.Lists.List.not_in_cons,Coq.Lists.List.nth_In,Coq.Lists.List.nth_S_cons,Coq.Lists.List.nth_default_eq,Coq.Lists.List.nth_error_In,Coq.Lists.List.nth_error_split,Coq.Lists.List.nth_indep,Coq.Lists.List.nth_overflow,Coq.Lists.List.nth_split,Coq.Lists.List.partition_cons1,Coq.Lists.List.partition_cons2,Coq.Lists.List.remove_In,Coq.Lists.List.removelast_app,Coq.Lists.List.rev_app_distr,Coq.Lists.List.rev_ind,Coq.Lists.List.rev_involutive,Coq.Lists.List.rev_length,Coq.Lists.List.rev_list_ind,Coq.Lists.List.rev_unit,Coq.Lists.List.skipn_O,Coq.Lists.List.skipn_cons,Coq.Lists.List.skipn_none,Coq.Lists.SetoidList.InA_InfA,Coq.Lists.SetoidList.InA_alt,Coq.Lists.SetoidList.InA_altdef,Coq.Lists.SetoidList.InA_app,Coq.Lists.SetoidList.InA_app_idem,Coq.Lists.SetoidList.InA_app_iff,Coq.Lists.SetoidList.InA_compat,Coq.Lists.SetoidList.InA_cons,Coq.Lists.SetoidList.InA_cons_hd,Coq.Lists.SetoidList.InA_cons_tl,Coq.Lists.SetoidList.InA_double_head,Coq.Lists.SetoidList.InA_eqA,Coq.Lists.SetoidList.InA_ind,Coq.Lists.SetoidList.InA_nil,Coq.Lists.SetoidList.InA_permute_heads,Coq.Lists.SetoidList.InA_rev,Coq.Lists.SetoidList.InA_sind,Coq.Lists.SetoidList.InA_split,Coq.Lists.SetoidList.In_InA,Coq.Lists.SetoidList.In_InfA,Coq.Lists.SetoidList.InfA_app,Coq.Lists.SetoidList.InfA_ltA,Coq.Lists.SetoidList.NoDupA_cons,Coq.Lists.SetoidList.NoDupA_ind,Coq.Lists.SetoidList.NoDupA_nil,Coq.Lists.SetoidList.NoDupA_rev,Coq.Lists.SetoidList.NoDupA_sind,Coq.Lists.SetoidList.NoDupA_split,Coq.Lists.SetoidList.NoDupA_swap,Coq.Lists.SetoidList.eqarefl,Coq.Lists.SetoidList.eqasym,Coq.Lists.SetoidList.eqlistA_altdef,Coq.Lists.SetoidList.eqlistA_app,Coq.Lists.SetoidList.eqlistA_cons,Coq.Lists.SetoidList.eqlistA_equiv,Coq.Lists.SetoidList.eqlistA_equivlistA,Coq.Lists.SetoidList.eqlistA_ind,Coq.Lists.SetoidList.eqlistA_length,Coq.Lists.SetoidList.eqlistA_rev,Coq.Lists.SetoidList.eqlistA_sind,Coq.Lists.SetoidList.equivlistA_NoDupA_split,Coq.Lists.SetoidList.equivlistA_app_idem,Coq.Lists.SetoidList.equivlistA_cons_nil,Coq.Lists.SetoidList.equivlistA_cons_proper,Coq.Lists.SetoidList.equivlistA_double_head,Coq.Lists.SetoidList.equivlistA_nil_eq,Coq.Lists.SetoidList.equivlistA_permute_heads,Coq.Lists.SetoidList.equivlist_equiv,Coq.Lists.SetoidList.filter_InA,Coq.Lists.SetoidList.fold_right_add,Coq.Lists.SetoidList.fold_right_add2,Coq.Lists.SetoidList.fold_right_add_restr,Coq.Lists.SetoidList.fold_right_add_restr2,Coq.Lists.SetoidList.fold_right_commutes,Coq.Lists.SetoidList.fold_right_commutes2,Coq.Lists.SetoidList.fold_right_commutes_restr,Coq.Lists.SetoidList.fold_right_commutes_restr2,Coq.Lists.SetoidList.fold_right_eqlistA2,Coq.Lists.SetoidList.fold_right_equivlistA,Coq.Lists.SetoidList.fold_right_equivlistA2,Coq.Lists.SetoidList.fold_right_equivlistA_restr,Coq.Lists.SetoidList.fold_right_equivlistA_restr2,Coq.Lists.SetoidList.incl_nil,Coq.Lists.SetoidList.removeA_InA,Coq.Lists.SetoidList.removeA_equivlistA,Coq.Logic.Decidable.dec_and,Coq.Logic.Decidable.dec_not_not,Coq.Logic.Decidable.dec_or,Coq.Logic.Decidable.not_and,Coq.Logic.Decidable.not_or,Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq,Coq.Logic.Eqdep.EqdepTheory.Streicher_K,Coq.Logic.Eqdep.EqdepTheory.UIP,Coq.Logic.Eqdep.EqdepTheory.eq_dep_eq,Coq.Logic.Eqdep.EqdepTheory.eq_rect_eq,Coq.Logic.EqdepFacts.eq_indd,Coq.Logic.EqdepFacts.internal_eq_sym_internal,Coq.Logic.Eqdep_dec.eq_proofs_unicity,Coq.Logic.Eqdep_dec.eq_proofs_unicity_on,Coq.Logic.FunctionalExtensionality.equal_f,Coq.Logic.FunctionalExtensionality.equal_f_dep,Coq.Logic.FunctionalExtensionality.eta_expansion,Coq.Logic.FunctionalExtensionality.eta_expansion_dep,Coq.Logic.FunctionalExtensionality.functional_extensionality,Coq.Logic.FunctionalExtensionality.functional_extensionality_dep,Coq.Logic.ProofIrrelevance.PI.proof_irrelevance,Coq.Logic.ProofIrrelevance.ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq,Coq.Logic.ProofIrrelevance.ProofIrrelevanceTheory.EqdepTheory.Streicher_K,Coq.Logic.ProofIrrelevance.ProofIrrelevanceTheory.EqdepTheory.UIP,Coq.Logic.ProofIrrelevance.ProofIrrelevanceTheory.EqdepTheory.eq_dep_eq,Coq.Logic.ProofIrrelevance.ProofIrrelevanceTheory.EqdepTheory.eq_rect_eq,Coq.Logic.ProofIrrelevance.ProofIrrelevanceTheory.eq_indd,Coq.Logic.ProofIrrelevance.proof_irrelevance,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_neq,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_refl,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_sym,Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_antisym,Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_irrefl,Coq.NArith.BinNat.N.Private_OrderTac.Tac.neq_eq,Coq.NArith.BinNat.N.Private_OrderTac.Tac.not_neq_eq,Coq.NArith.BinNat.N.Private_Tac.eq_neq,Coq.NArith.BinNat.N.Private_Tac.eq_refl,Coq.NArith.BinNat.N.Private_Tac.eq_sym,Coq.NArith.BinNat.N.Private_Tac.le_antisym,Coq.NArith.BinNat.N.Private_Tac.neq_eq,Coq.NArith.BinNat.N.Private_Tac.neq_sym,Coq.NArith.BinNat.N.Private_Tac.not_neq_eq,Coq.NArith.BinNat.N.eq_equiv,Coq.NArith.BinNat.N.eq_stepl,Coq.NArith.BinNat.N.le_0_l,Coq.NArith.BinNat.N.le_antisymm,Coq.NArith.BinNat.N.lt_trichotomy,Coq.NArith.BinNat.N.neq_sym,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.neq_eq,Coq.PArith.BinPos.Pos.Private_Tac.neq_sym,Coq.PArith.BinPos.Pos.Private_Tac.not_neq_eq,Coq.PArith.BinPos.Pos.add_1_l,Coq.PArith.BinPos.Pos.add_comm,Coq.PArith.BinPos.Pos.add_succ_l,Coq.PArith.BinPos.Pos.compare_spec,Coq.PArith.BinPos.Pos.iter_swap_gen,Coq.PArith.BinPos.Pos.peano_ind,Coq.PArith.BinPos.Pos.sub_add,Coq.QArith.QArith_base.Q_Setoid,Coq.QArith.QArith_base.Qeq_bool_eq,Coq.Relations.Relation_Operators.Desc_ind,Coq.Relations.Relation_Operators.Desc_sind,Coq.Relations.Relation_Operators.Lt_hd,Coq.Relations.Relation_Operators.Lt_nil,Coq.Relations.Relation_Operators.Lt_tl,Coq.Relations.Relation_Operators.Ltl_ind,Coq.Relations.Relation_Operators.Ltl_sind,Coq.Relations.Relation_Operators.d_conc,Coq.Setoids.Setoid.Build_Setoid_Theory,Coq.Setoids.Setoid.Seq_refl,Coq.Setoids.Setoid.Seq_sym,Coq.Setoids.Setoid.Seq_trans,Coq.Sorting.Sorted.HdRel_cons,Coq.Sorting.Sorted.HdRel_ind,Coq.Sorting.Sorted.HdRel_inv,Coq.Sorting.Sorted.HdRel_nil,Coq.Sorting.Sorted.HdRel_sind,Coq.Sorting.Sorted.LSorted_cons1,Coq.Sorting.Sorted.LSorted_consn,Coq.Sorting.Sorted.LocallySorted_ind,Coq.Sorting.Sorted.LocallySorted_sind,Coq.Sorting.Sorted.SSorted_cons,Coq.Sorting.Sorted.Sorted_StronglySorted,Coq.Sorting.Sorted.Sorted_cons,Coq.Sorting.Sorted.Sorted_extends,Coq.Sorting.Sorted.Sorted_ind,Coq.Sorting.Sorted.Sorted_inv,Coq.Sorting.Sorted.Sorted_sind,Coq.Sorting.Sorted.StronglySorted_Sorted,Coq.Sorting.Sorted.StronglySorted_ind,Coq.Sorting.Sorted.StronglySorted_sind,Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_refl,Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_sym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_neq,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_refl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_sym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_antisym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_refl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_irrefl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_eq,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_sym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_ge_lt,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_gt_le,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_neq_eq,Coq.ZArith.BinInt.Z.Private_Tac.eq_neq,Coq.ZArith.BinInt.Z.Private_Tac.eq_refl,Coq.ZArith.BinInt.Z.Private_Tac.eq_sym,Coq.ZArith.BinInt.Z.Private_Tac.le_antisym,Coq.ZArith.BinInt.Z.Private_Tac.neq_eq,Coq.ZArith.BinInt.Z.Private_Tac.neq_sym,Coq.ZArith.BinInt.Z.Private_Tac.not_neq_eq,Coq.ZArith.BinInt.Z.add_0_l,Coq.ZArith.BinInt.Z.add_0_r,Coq.ZArith.BinInt.Z.add_comm,Coq.ZArith.BinInt.Z.eq_decidable,Coq.ZArith.BinInt.Z.eq_equiv,Coq.ZArith.BinInt.Z.eq_stepl,Coq.ZArith.BinInt.Z.eq_sym_iff,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.lt_decidable,Coq.ZArith.BinInt.Z.lt_eq_cases,Coq.ZArith.BinInt.Z.lt_trichotomy,Coq.ZArith.BinInt.Z.max_spec,Coq.ZArith.BinInt.Z.mul_comm,Coq.ZArith.BinInt.Z.neq_sym,Coq.ZArith.BinInt.Z.opp_inj,Coq.ZArith.BinInt.Z.pos_sub_discr,Coq.ZArith.Zbool.Zeq_bool_eq,Coq.ZArith.Zcomplements.Zlength_cons,Coq.ZArith.Zcomplements.Zlength_correct,Coq.ZArith.Zcomplements.Zlength_nil_inv,Coq.ZArith.Znat.Nat2Z.inj_0,Coq.ZArith.Znat.Nat2Z.inj_iff,Coq.ZArith.Znat.Nat2Z.inj_succ,Coq.ZArith.Znat.Nat2Z.is_nonneg,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.Zle_left,Coq.ZArith.auxiliary.Zlt_left,Coq.ZArith.auxiliary.Zne_left,Coq.micromega.OrderedRing.SORrt,Coq.micromega.OrderedRing.ropp_morph_Proper,Coq.micromega.OrderedRing.rplus_morph_Proper,Coq.micromega.OrderedRing.rtimes_morph_Proper,Coq.micromega.OrderedRing.sor_setoid_Reflexive,Coq.micromega.OrderedRing.sor_setoid_Symmetric,Coq.micromega.Refl.make_conj_app,Coq.micromega.Refl.make_conj_cons,Coq.micromega.Refl.make_conj_impl,Coq.micromega.Refl.make_conj_in,Coq.micromega.Refl.make_impl_true,Coq.micromega.Refl.not_make_conj_cons,Coq.micromega.RingMicromega.micomega_sor_setoid_Reflexive,Coq.micromega.RingMicromega.micomega_sor_setoid_Symmetric,Coq.micromega.RingMicromega.micomega_sor_setoid_Transitive,Coq.micromega.RingMicromega.ropp_morph_Proper,Coq.micromega.RingMicromega.rplus_morph_Proper,Coq.micromega.RingMicromega.rtimes_morph_Proper,Coq.micromega.Tauto.map_simpl,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.E_ST,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.add_iff,Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.dec_eq,Coq.omega.OmegaLemmas.OMEGA17,Coq.omega.OmegaLemmas.OMEGA2,Coq.omega.OmegaLemmas.OMEGA6,Coq.omega.OmegaLemmas.OMEGA8,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_factor5,Coq.omega.OmegaLemmas.intro_Z,Coq.omega.OmegaLemmas.new_var,Coq.setoid_ring.BinList.jump_add,Coq.setoid_ring.BinList.jump_pred_double,Coq.setoid_ring.BinList.jump_tl,Coq.setoid_ring.Field_theory.AF_1_neq_0,Coq.setoid_ring.Field_theory.AF_AR,Coq.setoid_ring.Field_theory.AFdiv_def,Coq.setoid_ring.Field_theory.AFinv_l,Coq.setoid_ring.Field_theory.F_R,Coq.setoid_ring.Field_theory.NPEequiv_eq,Coq.setoid_ring.Field_theory.PCond_app,Coq.setoid_ring.Field_theory.PCond_cons,Coq.setoid_ring.Field_theory.PCond_cons_inv_l,Coq.setoid_ring.Field_theory.PCond_cons_inv_r,Coq.setoid_ring.Field_theory.absurd_PCond_bottom,Coq.setoid_ring.Field_theory.ceqb_spec,Coq.setoid_ring.Field_theory.field_is_integral_domain,Coq.setoid_ring.Field_theory.radd_ext_Proper,Coq.setoid_ring.Field_theory.rdiv1,Coq.setoid_ring.Field_theory.rdiv8,Coq.setoid_ring.Field_theory.rdiv_ext,Coq.setoid_ring.Field_theory.rdiv_r_r,Coq.setoid_ring.Field_theory.rinv_ext_Proper,Coq.setoid_ring.Field_theory.rinv_nz,Coq.setoid_ring.Field_theory.rmul_ext_Proper,Coq.setoid_ring.Field_theory.rmul_reg_l,Coq.setoid_ring.Field_theory.ropp_ext_Proper,Coq.setoid_ring.Field_theory.ropp_neq_0,Coq.setoid_ring.InitialRing.Neqb_ok,Coq.setoid_ring.InitialRing.R_setoid5_Reflexive,Coq.setoid_ring.InitialRing.Ztriv_div_th,Coq.setoid_ring.InitialRing.gen_phiNword_cons,Coq.setoid_ring.InitialRing.get_signZ_th,Coq.setoid_ring.InitialRing.radd_ext5_Proper,Coq.setoid_ring.Ring.bool_eq_ok,Coq.setoid_ring.Ring_polynom.Pphi0,Coq.setoid_ring.Ring_polynom.Pphi1,Coq.setoid_ring.Ring_polynom.ceqb_spec,Coq.setoid_ring.Ring_polynom.jump_add',Coq.setoid_ring.Ring_polynom.radd_ext_Proper,Coq.setoid_ring.Ring_polynom.rmul_ext_Proper,Coq.setoid_ring.Ring_polynom.ropp_ext_Proper,Coq.setoid_ring.Ring_theory.ARadd_0_l,Coq.setoid_ring.Ring_theory.ARadd_0_r,Coq.setoid_ring.Ring_theory.ARadd_assoc,Coq.setoid_ring.Ring_theory.ARadd_assoc1,Coq.setoid_ring.Ring_theory.ARadd_assoc2,Coq.setoid_ring.Ring_theory.ARadd_comm,Coq.setoid_ring.Ring_theory.ARdistr_l,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_assoc1,Coq.setoid_ring.Ring_theory.ARmul_assoc2,Coq.setoid_ring.Ring_theory.ARmul_comm,Coq.setoid_ring.Ring_theory.ARopp_add,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.ARth_SRth,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.IDmorph,Coq.setoid_ring.Ring_theory.Radd_ext,Coq.setoid_ring.Ring_theory.Rmul_ext,Coq.setoid_ring.Ring_theory.Rth_ARth,Coq.setoid_ring.Ring_theory.SReqe_Reqe,Coq.setoid_ring.Ring_theory.SRth_ARth,Coq.setoid_ring.Ring_theory.get_sign_None_th,Coq.setoid_ring.Ring_theory.mk_reqe,Coq.setoid_ring.Ring_theory.mk_seqe,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,ExtLib.Data.Member.member_In,ExtLib.Data.Member.member_case,ExtLib.Data.Member.member_eta,ExtLib.Data.Member.member_ind,ExtLib.Tactics.EqDep.UIP_refl,HList.app_ass_trans,HList.app_nil_r_trans,HList.hlist.Reflexive_equiv_hlist,HList.hlist.Symmetric_equiv_hlist,HList.hlist.Transitive_equiv_hlist,HList.hlist.equiv_hlist_Hcons,HList.hlist.equiv_hlist_app,HList.hlist.equiv_hlist_ind,HList.hlist.hlist_app_nil_r,HList.hlist.hlist_cons_eta,HList.hlist.hlist_eqv_cons,HList.hlist.hlist_eqv_nil,HList.hlist.hlist_eta,HList.hlist.hlist_ind,HList.hlist.hlist_nil_eta,HList.hlist.hlist_rev_nil,$adef_Coq.Arith.PeanoNat.Nat.eqf_$a2,$adef_Coq.Lists.List.seq_$a2,$adef_Coq.setoid_ring.Ring_theory.SRopp_$a1,$adef_$_prop_34460_$a4,$adef_$_prop_15659_$a4,$adef_Coq.Reals.Rdefinitions.IZR_$a1,$adef_Coq.Init.Datatypes.None_$a1,$adef_Coq.NArith.BinNat.N.lt_$a2,$adef_$_prop_126684_$a7,$adef_Coq.ZArith.BinIntDef.Z.of_N_$a1,$adef_Coq.Vectors.VectorDef.cons_$a4,$adef_Coq.setoid_ring.Ring_polynom.Pequiv_$a9,$adef_Coq.ZArith.BinIntDef.Z.modulo_$a2,$adef_Coq.Init.Datatypes.BoolSpec_$a3,$adef_Coq.setoid_ring.Ring_theory.SRopp_$a2,$adef_Coq.Lists.List.repeat_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.rev_$a1,$adef_$_prop_16608_$a3,$adef_Coq.Lists.List.Exists_$a3,$adef_Coq.micromega.Tauto.cons_id_$a3,$adef_Coq.setoid_ring.Ring_polynom.mk_monpol_list_$a10,$adef_Coq.setoid_ring.Field_theory.NPEequiv_$a15,$adef_Coq.micromega.RingMicromega.PsatzMulC_$a3,$adef_Coq.Reals.Rfunctions.ZintPos_$a2,$adef_$_prop_116341_$a3,$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.Lists.List.count_occ_$a4,$adef_Coq.micromega.EnvRing.Pol_$a1,$adef_HList.hlist.Injection_equiv_hlist_cons_$a7,$adef_Coq.micromega.Tauto.eval_tt_$a5,$adef_Coq.micromega.Tauto.Cj_$a6,$adef_Coq.setoid_ring.Ring_polynom.PEmul_$a3,$adef_Coq.Relations.Relation_Operators.clos_refl_$a4,$adef_HList.hlist.hlist_$a1,$adef_Coq.Lists.List.partition_$a3,$adef_Coq.Lists.List.nth_error_$a3,$adef_Coq.setoid_ring.Ring_polynom.Pc_$a2,$adef_Coq.micromega.RMicromega.CMult_$a2,$adef_Coq.Sorting.Sorted.LocallySorted_$a3,$adef_Coq.setoid_ring.Ring_polynom.vmon_$a2,$adef_Coq.Lists.SetoidList.inclA_$a4,$adef_$_lam_17912_$a5,$adef_Coq.Logic.JMeq.JMeq_$a4,$adef_Coq.setoid_ring.BinList.nth_$a4,$adef_$_case_Coq.Numbers.BinNums.Z$120576_$a3,$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.Init.Datatypes.CompareSpecT_$a4,$adef_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_elt_Prop_$a1,$adef_$_prop_15769_$a3,$adef_Coq.setoid_ring.Field_theory.FEdiv_$a3,$adef_$_prop_15517_$a2,$adef_Coq.setoid_ring.Ring_theory.almost_ring_theory_$a8,$adef_Coq.Init.Specif.projT2_$a3,$adef_Coq.micromega.Tauto.collect_annot_$a5,$adef_$_lam_47639_$a3,$adef_Coq.micromega.Tauto.eval_f_$a7,$adef_Coq.Init.Datatypes.app_$a3,$adef_Coq.setoid_ring.InitialRing.gen_phiZ_$a7,$adef_Coq.Init.Specif.existT_$a4,$adef_$_prop_126634_$a7,$adef_Coq.Init.Specif.sig_$a2,$adef_Coq.ZArith.BinIntDef.Z.leb_$a2,$adef_$_let_var_var_7_n_15725_15729_15738_$a4,$adef_$_case_Coq.Init.Datatypes.list$505_$a3,$adef_Coq.PArith.BinPosDef.Pos.pred_double_$a1,$adef_Coq.setoid_ring.Field_theory.Fapp_$a4,$adef_Coq.setoid_ring.Field_theory.FEmul_$a3,$adef_Coq.ZArith.BinIntDef.Z.mul_$a2,$adef_Coq.micromega.ZMicromega.EnumProof_$a3,$adef_Coq.PArith.BinPosDef.Pos.iter_$a4,$adef_Coq.micromega.RingMicromega.Build_Formula_$a4,$adef_Coq.setoid_ring.Ring_polynom.mkmult_pow_$a5,$adef_Coq.Init.Specif.sumbool_$a2,$adef_$_prop_15697_$a3,$adef_Coq.Classes.RelationClasses.StrictOrder_$a2,$adef_Coq.setoid_ring.Field_theory.mk_rsplit_$a4,$adef_Coq.Lists.List.last_$a3,$adef_Coq.setoid_ring.Ring_theory.semi_ring_theory_$a6,$adef_$_prop_45254_$a2,$adef_Coq.micromega.RingMicromega.check_inconsistent_$a4,$adef_Coq.Lists.SetoidList.transpose_restr2_$a5,$adef_Coq.Init.Specif.proj1_sig_$a3,$adef_Coq.setoid_ring.Ring_polynom.PEsub_$a3,$adef_Coq.Lists.List.existsb_$a3,$adef_$_prop_126660_$a7,$adef_Coq.Init.Nat.max_$a2,$adef_Coq.Lists.List.hd_$a3,$adef_Coq.Init.Datatypes.option_$a1,$adef_$_prop_15771_$a3,$adef_Coq.Relations.Relation_Definitions.relation_$a1,$adef_Coq.setoid_ring.Ring_polynom.Pphi_$a8,$adef_$_generic_case_48326_$a1,$adef_Coq.setoid_ring.Ring_polynom.Peq_$a4,$adef_Coq.Lists.List.forallb_$a3,$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_Coq.setoid_ring.Field_theory.Fcons_$a4,$adef_Coq.Lists.List.skipn_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.rev_append_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_morph_$a17,$adef_Coq.Init.Datatypes.CompOpp_$a1,$adef_Coq.micromega.EnvRing.PEopp_$a2,$adef_Coq.micromega.RingMicromega.SORaddon_$a22,$adef_Coq.ZArith.Zpower.two_power_pos_$a1,$adef_Coq.Init.Logic.and_rect_$a5,$adef_$_prop_15698_$a3,$adef_Coq.setoid_ring.Field_theory.FExpr_$a1,$adef_$_lam_38194_$a4,$adef_Coq.micromega.RingMicromega.PolEnv_$a1,$adef_$_lam_24987_$a11,$adef_$_case_Coq.setoid_ring.Ring_polynom.Pol$12766_$a20,$adef_ExtLib.Data.Member.member_$a3,$adef_Coq.Reals.Rdefinitions.Rle_$a2,$adef_Coq.setoid_ring.Field_theory.split_$a7,$adef_Coq.micromega.Tauto.eval_cnf_$a6,$adef_Coq.setoid_ring.Ring_polynom.interp_PElist_$a15,$adef_HList.hlist.hlist_rev'_$a4,$adef_Coq.micromega.EnvRing.zmon_$a2,$adef_$_let_18_mkmult_pow_28089_$a6,$adef_Coq.setoid_ring.Ring_polynom.mkPinj_$a3,$adef_Coq.Logic.EqdepFacts.eq_dep_$a6,$adef_Coq.setoid_ring.Ring_theory.div_theory_$a7,$adef_$_lam_46514_$a2,$adef_Coq.Sorting.Sorted.HdRel_$a4,$adef_Coq.setoid_ring.Field_theory.display_pow_linear_$a20,$adef_$_lam_17912_$a4,$adef_Coq.Reals.Rfunctions.Z_spec_$a2,$adef_Coq.Init.Datatypes.inl_$a3,$adef_$_lam_16675_$a5,$adef_Coq.setoid_ring.Ring_polynom.mkZmon_$a2,$adef_Coq.NArith.BinNat.N.divide_$a2,$adef_Coq.Lists.SetoidList.transpose2_$a4,$adef_Coq.Vectors.VectorDef.of_list_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_eq_ext_$a5,$adef_Coq.setoid_ring.Field_theory.Fcons2_$a11,$adef_Coq.Vectors.VectorDef.to_list_$a3,$adef_Coq.Logic.EqdepFacts.Streicher_K_on__$a3,$adef_$_prop_116344_$a3,$adef_Coq.Logic.EqdepFacts.Eq_dep_eq_on_$a4,$adef_Coq.setoid_ring.Ring.bool_eq_$a2,$adef_Coq.Lists.SetoidList.equivlistA_$a2,$adef_Coq.Lists.List.Forall2_$a5,$adef_Coq.Reals.Rdefinitions.Rdiv_$a2,$adef_$_prop_46989_$a4,$adef_Coq.Init.Datatypes.nil_$a1,$adef_Coq.Logic.EqdepFacts.eq_dep1_$a6,$adef_HList.hlist.hlist_tl_$a3,$adef_Coq.Init.Datatypes.cons_$a1,$adef_$_lam_15512_$a3,$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.list_rec_$a2,$adef_Coq.ZArith.Znumtheory.Bezout_$a3,$adef_Coq.micromega.Tauto.GFormula_$a4,$adef_Coq.micromega.Tauto.cnf_$a2,$adef_Coq.Numbers.BinNums.Npos_$a1,$adef_Coq.setoid_ring.Ring_theory.Morphism_$a17,$adef_Coq.setoid_ring.Ring_theory.IDphi_$a2,$adef_Coq.setoid_ring.Field_theory.PEsimp_$a9,$adef_Coq.setoid_ring.Field_theory.Fcons1_$a11,$adef_Coq.setoid_ring.Ring_polynom.P0_$a2,$adef_Coq.setoid_ring.Ring_theory.SRsub_$a2,$adef_$_prop_34493_$a4,$adef_Coq.Numbers.BinNums.xI_$a1,$adef_$_case_Coq.Init.Datatypes.nat$120559_$a3,$adef_HList.hlist.hlist_rect_$a1,$adef_$_let_16_mkpow_28087_$a5,$adef_Coq.micromega.RMicromega.CPow_$a2,$adef_Coq.setoid_ring.Field_theory.condition_$a2,$adef_Coq.micromega.RMicromega.CPlus_$a2,$adef_Coq.setoid_ring.Ring_theory.IDphi_$a1,$adef_Coq.Lists.List.rev'_$a2,$adef_Coq.Init.Datatypes.negb_$a1,$adef_Coq.micromega.RMicromega.COpp_$a1,$adef_HList.hlist.hlist_app_$a4,$adef_Coq.Reals.Rdefinitions.Ropp_$a1,$adef_$_lam_2042_$a3,$adef_Coq.setoid_ring.Ring_polynom.PEeval_$a14,$adef_$_let_11_subst_l_24915_$a10,$adef_Coq.Lists.List.combine_$a4,$adef_HList.hlist.hlist_rev'_$a3,$adef_Coq.setoid_ring.Ring_polynom.P1_$a2,$adef_Coq.Arith.Even.odd_$a1,$adef_$_lam_24987_$a12,$adef_Coq.Lists.List.ForallOrdPairs_$a3,$adef_Coq.ZArith.BinIntDef.Z.succ_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.add_$a2,$adef_$_lam_17884_$a3,$adef_Coq.Lists.List.split_$a3,$adef_Coq.Init.Nat.add_$a2,$adef_Coq.Init.Specif.sigT2_$a3,$adef_Coq.setoid_ring.Field_theory.display_linear_$a17,$adef_Coq.ZArith.Zcomplements.Zlength_$a2,$adef_$_lam_34982_$a7,$adef_Coq.Structures.OrderedType.Compare_$a5,$adef_HList.hlist.hlist_rec_$a1,$adef_Coq.setoid_ring.Field_theory.FEc_$a2,$adef_Coq.Classes.Morphisms.Proper_$a3,$adef_$_lam_48310_$a6,$adef_Coq.Reals.Rdefinitions.Rminus_$a2,$adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2,$adef_Coq.setoid_ring.Ring_polynom.Pphi_pow_$a18,$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_ExtLib.Data.Member.member_rec_$a3,$adef_Coq.Lists.List.ForallPairs_$a3,$adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3,$adef_Coq.Classes.RelationClasses.eq_equivalence_$a1,$adef_Coq.Sorting.Sorted.StronglySorted_$a3,$adef_$_lam_48310_$a7,$adef_Coq.Reals.Rdefinitions.Rplus_$a2,$adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2,$adef_Coq.Lists.List.Add_$a4,$adef_Coq.micromega.RMicromega.CMinus_$a2,$adef_Coq.Lists.List.rev_$a2,$adef_$_lam_35023_$a7,$adef_Coq.setoid_ring.Field_theory.FEadd_$a3,$adef_Coq.Init.Datatypes.S_$a1,$adef_$_lam_34898_$a4,$adef_Coq.Strings.Ascii.Ascii_$a8,$adef_$_case_Coq.Init.Datatypes.list$35694_$a4,$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_HList.hlist.hlist_app_$a3,$adef_Coq.micromega.RingMicromega.Formula_$a1,$adef_Coq.setoid_ring.Ring_theory.SRsub_$a4,$adef_Coq.micromega.ZMicromega.RatProof_$a2,$adef_HList.hlist.hlist_rev_$a2,$adef_Coq.micromega.RingMicromega.PolC_$a1,$adef_Coq.Sorting.Sorted.StronglySorted_rect_$a6,$adef_Coq.Lists.SetoidList.InA_$a4,$adef_$_lam_16646_$a6,$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.Strings.String.list_ascii_of_string_$a1,$adef_Coq.setoid_ring.Ring_polynom.Pphi_avoid_$a15,$adef_Coq.Lists.List.firstn_$a3,$adef_Coq.setoid_ring.Field_theory.mk_linear_$a4,$adef_Coq.setoid_ring.Ring_theory.pow_pos_$a4,$adef_Coq.Relations.Relation_Operators.Ltl_$a4,$adef_$_prop_15696_$a3,$adef_Coq.Init.Nat.pow_$a2,$adef_Coq.micromega.Tauto.I_$a7,$adef_Coq.micromega.Refl.make_conj_$a3,$adef_Coq.ZArith.BinInt.Z.gt_$a2,$adef_Coq.Classes.RelationClasses.Symmetric_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEO_$a1,$adef_Coq.Init.Logic.eq_rect_$a5,$adef_Coq.Lists.List.flat_map_$a4,$adef_Coq.Numbers.BinNums.xO_$a1,$adef_$_prop_116342_$a3,$adef_Coq.Reals.Rdefinitions.Rinv_$a1,$adef_Coq.Lists.SetoidList.transpose_restr_$a5,$adef_HList.hlist.equiv_hlist_app_$a7,$adef_ExtLib.Data.Member.get_next_$a5,$adef_Coq.QArith.QArith_base.Qdiv_$a2,$adef_Coq.ZArith.Zpower.Zdiv_rest_proof_$a4,$adef_Coq.setoid_ring.Field_theory.FEinv_$a2,$adef_Coq.setoid_ring.Ring_theory.pow_N_$a5,$adef_$_let_var_6_p_28809_28811_$a4,$adef_Coq.ZArith.BinInt.Z.ge_$a2,$adef_Coq.QArith.QArith_base.Qeq_$a2,$adef_Coq.ZArith.Zbool.Zeq_bool_$a2,$adef_Coq.micromega.RMicromega.CQ_$a1,$adef_Coq.QArith.QArith_base.Qmake_$a2,$adef_Coq.Init.Specif.sumbool_rect_$a3,$adef_$_case_Coq.Init.Datatypes.prod$33222_$a9,$adef_Coq.micromega.EnvRing.PEc_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEX_$a2,$adef_$_lam_17884_$a2,$adef_ExtLib.Data.Member.member_rect_$a3,$adef_$_let_17_lnum_11934_$a15,$adef_Coq.micromega.OrderedRing.SOR_$a10,$adef_Coq.Init.Datatypes.sum_$a2,$adef_Coq.setoid_ring.Field_theory.FEeval_$a16,$adef_$_prop_37890_$a2,$adef_Coq.ZArith.Znumtheory.Zis_gcd_$a3,$adef_Coq.setoid_ring.Field_theory.absurd_PCond_$a2,$adef_$_prop_37864_$a2,$adef_Coq.setoid_ring.Ring_polynom.norm_aux_$a9,$adef_Coq.setoid_ring.InitialRing.triv_div_$a6,$adef_$_let_var_6_p_28807_28810_$a4,$adef_Coq.Vectors.Fin.t_$a1,$adef_Coq.setoid_ring.Field_theory.FEO_$a1,$adef_Coq.setoid_ring.Field_theory.rsplit_common_$a2,$adef_Coq.Init.Logic.proj2_$a3,$adef_Coq.Lists.List.In_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.Empty_$a1,$adef_Coq.Init.Datatypes.andb_$a2,$adef_Coq.Init.Peano.lt_$a2,$adef_$_fix_36692_v_CANONICAL_2_$a5,$adef_$_case_Coq.Init.Datatypes.nat$120581_$a1,$adef_Coq.micromega.ZMicromega.CutProof_$a2,$adef_Coq.ZArith.BinIntDef.Z.max_$a2,$adef_Coq.Init.Nat.mul_$a2,$adef_$_lam_16675_$a3,$adef_Coq.micromega.Tauto.eval_clause_$a5,$adef_Coq.Init.Peano.le_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.Node_$a3,$adef_Coq.Arith.PeanoNat.Nat.divide_$a2,$adef_$_case_Coq.Init.Datatypes.list$418_$a6,$adef_Coq.setoid_ring.Field_theory.rsplit_$a1,$adef_ExtLib.Tactics.Injection.Injective_$a1,$adef_Coq.Classes.RelationClasses.Equivalence_$a2,$adef_Coq.Arith.Even.even_$a1,$adef_Coq.micromega.ZMicromega.is_pol_Z0_$a1,$adef_Coq.micromega.Tauto.TT_$a4,$adef_Coq.Logic.Decidable.decidable_$a1,$adef_$_case_Coq.Init.Datatypes.list$46502_$a1,$adef_ExtLib.Core.RelDec.Build_RelDec_$a3,$adef_$_let_17_mkopp_pow_28088_$a6,$adef_Coq.micromega.EnvRing.PEmul_$a3,$adef_Coq.Init.Datatypes.snd_$a3,$adef_Coq.QArith.QArith_base.Qeq_bool_$a2,$adef_Coq.ZArith.BinInt.Z.eqf_$a2,$adef_Coq.QArith.QArith_base.Qmult_$a2,$adef_Coq.PArith.BinPos.Pos.lt_$a2,$adef_Coq.NArith.BinNatDef.N.testbit_$a2,$adef_Coq.PArith.BinPosDef.Pos.to_nat_$a1,$adef_$_prop_126659_$a7,$adef_Coq.Init.Datatypes.CompLtT_$a3,$adef_Coq.Lists.List.nth_$a4,$adef_Coq.Lists.SetoidList.transpose_$a4,$adef_$_prop_15624_$a3,$adef_Coq.Init.Datatypes.inr_$a3,$adef_$_prop_16926_$a3,$adef_Coq.setoid_ring.Ring_polynom.Pphi_dev_$a15,$adef_HList.hlist.Injection_equiv_hlist_app_$a7,$adef_Coq.Vectors.Fin.F1_$a1,$adef_Coq.QArith.QArith_base.Qnum_$a1,$adef_HList.hlist.hlist_rect_$a5,$adef_ExtLib.Data.Member.MN_$a5,$adef_Coq.Lists.List.remove_$a4,$adef_Coq.setoid_ring.Ring_polynom.PNSubstL_$a11,$adef_Coq.Lists.List.lel_$a3,$adef_$_lam_46514_$a3,$adef_$_lam_46511_$a1,$adef_$_prop_15623_$a3,$adef_Coq.PArith.BinPosDef.Pos.succ_$a1,$adef_Coq.setoid_ring.Field_theory.FEsub_$a3,$adef_$_lam_2046_$a4,$adef_Coq.Relations.Relation_Operators.Desc_$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.xelements_$a3,$adef_ExtLib.Data.Member.MZ_$a3,$adef_Coq.micromega.Tauto.D_$a6,$adef_$_prop_15699_$a3,$adef_Coq.Init.Datatypes.prod_$a2,$adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a12,$adef_Coq.setoid_ring.InitialRing.Nwadd_$a2,$adef_Coq.ZArith.BinIntDef.Z.compare_$a2,$adef_$_case_Coq.Init.Datatypes.list$17865_$a3,$adef_Coq.setoid_ring.Ring_theory.ring_theory_$a8,$adef_Coq.QArith.QArith_base.Qden_$a1,$adef_Coq.Lists.List.rev_append_$a3,$adef_Coq.setoid_ring.InitialRing.gen_phiPOS_$a5,$adef_Coq.micromega.Tauto.eval_tt_$a6,$adef_Coq.micromega.ZMicromega.valid_cut_sign_$a1,$adef_$_case_Coq.Init.Datatypes.list$46502_$a2,$adef_Coq.Lists.List.concat_$a2,$adef_$_lam_47646_$a7,$adef_$_let_20_lnum_12462_$a18,$adef_$_prop_116343_$a3,$adef_Coq.NArith.BinNatDef.N.div_eucl_$a2,$adef_Coq.micromega.RMicromega.CZ_$a1,$adef_$_prop_15768_$a3,$adef_Coq.ZArith.BinInt.Z.lt_$a2,$adef_Coq.setoid_ring.Field_theory.linear_$a1,$adef_$_lam_2046_$a3,$adef_Coq.PArith.BinPosDef.Pos.eqb_$a2,$adef_HList.hlist.equiv_hlist_$a2,$adef_Coq.setoid_ring.Field_theory.PCond_$a15,$adef_Coq.ZArith.BinIntDef.Z.opp_$a1,$adef_ExtLib.Data.Member.member_rect_$a7,$adef_Coq.setoid_ring.Ring_polynom.r_list_pow_$a4,$adef_Coq.Numbers.BinNums.Zneg_$a1,$adef_Coq.micromega.RingMicromega.ge_bool_$a2,$adef_Coq.QArith.QArith_base.Qminus_$a2,$adef_Coq.Reals.Rdefinitions.Rgt_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3,$adef_Coq.NArith.BinNatDef.N.to_nat_$a1,$adef_Coq.Classes.RelationClasses.Transitive_$a2,$adef_Coq.ZArith.BinIntDef.Z.double_$a1,$adef_Coq.Bool.Bool.reflect_$a2,$adef_Coq.Sets.Relations_1.Transitive_$a2,$adef_Coq.setoid_ring.Ring_polynom.PX_$a4,$adef_Coq.setoid_ring.Field_theory.Fcons0_$a11,$adef_$_lam_34898_$a3,$adef_Coq.setoid_ring.InitialRing.Nwcons_$a2,$adef_Coq.micromega.RingMicromega.PsatzIn_$a2,$adef_Coq.setoid_ring.Field_theory.NPEopp_$a3,$adef_Coq.PArith.BinPosDef.Pos.sub_mask_$a2,$adef_$_case_Coq.Init.Specif.sumbool$15756_$a5,$adef_Coq.Init.Specif.inright_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEI_$a1,$adef_Coq.ZArith.Zcomplements.Zlength_aux_$a3,$adef_Coq.ZArith.BinIntDef.Z.gtb_$a2,$adef_$_case_Coq.setoid_ring.Ring_polynom.Pol$12167_$a17,$adef_Coq.NArith.BinNatDef.N.pos_div_eucl_$a2,$adef_$_lam_16626_$a1,$adef_Coq.ZArith.Zcomplements.Zlength_aux_$a1,$adef_Coq.setoid_ring.Ring_theory.get_sign_None_$a1,$adef_HList.hlist.equiv_hlist_Hcons_$a7,$adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3,$adef_Coq.micromega.Tauto.cnf_checker_$a6,$adef_$_prop_16617_$a3,$adef_Coq.setoid_ring.Field_theory.FEopp_$a2,$adef_Coq.Lists.SetoidList.eqlistA_$a4,$adef_Coq.Init.Specif.exist2_$a4,$adef_Coq.Init.Datatypes.CompareSpec_$a4,$adef_Coq.Init.Datatypes.xorb_$a2,$adef_$_prop_122450_$a2,$adef_$_fix_37630_1_add_carry_$a2,$adef_Coq.Strings.String.String_$a2,$adef_$_lam_47639_$a2,$adef_Coq.setoid_ring.Field_theory.split_aux_$a8,$adef_Coq.ZArith.Znumtheory.Euclid_intro_$a5,$adef_Coq.Init.Datatypes.CompEqT_$a3,$adef_Coq.micromega.RingMicromega.PsatzMulE_$a3,$adef_Coq.Classes.Morphisms.respectful_$a4,$adef_Coq.Init.Specif.sumbool_rec_$a3,$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.NArith.BinNatDef.N.succ_$a1,$adef_Coq.Lists.List.in_dec_$a4,$adef_Coq.Init.Datatypes.list_rect_$a2,$adef_Coq.Structures.OrderedType.GT_$a5,$adef_$_let_17_mkopp_pow_28088_$a8,$adef_Coq.setoid_ring.Ring_polynom.Pphi_pow_$a16,$adef_ExtLib.Structures.Functor.ID_$a2,$adef_Coq.ZArith.BinIntDef.Z.succ_double_$a1,$adef_Coq.Sorting.Sorted.StronglySorted_inv_$a4,$adef_Coq.setoid_ring.Ring_theory.id_phi_N_$a1,$adef_Coq.Vectors.Fin.FS_$a2,$adef_$_prop_16616_$a3,$adef_HList.hlist.hlist_hd_$a3,$adef_ExtLib.Core.RelDec.RelDec_$a2,$adef_Coq.micromega.EnvRing.PExpr_$a1,$adef_$_lam_126658_$a7,$adef_$_lam_34982_$a4,$adef_Coq.Setoids.Setoid.Setoid_Theory_$a2,$adef_Coq.setoid_ring.Field_theory.rsplit_right_$a2,$adef_Coq.setoid_ring.BinList.jump_$a3,$adef_Coq.Init.Peano.ge_$a2,$adef_F_$a1,$adef_ExtLib.Tactics.Injection.Build_Injective_$a2,$adef_Coq.Strings.String.string_of_list_ascii_$a1,$adef_Coq.setoid_ring.InitialRing.get_signZ_$a1,$adef_Coq.Lists.SetoidList.NoDupA_$a3,$adef_Coq.Init.Datatypes.list_rect_$a5,$adef_Coq.Logic.EqdepFacts.UIP_on__$a3,$adef_Coq.setoid_ring.InitialRing.gen_phiNword_$a8,$adef_Coq.Classes.RelationClasses.Reflexive_$a2,$adef_Coq.micromega.Tauto.A_$a6,$adef_$_lam_15516_$a4,$adef_Coq.micromega.EnvRing.vmon_$a2,$adef_Coq.micromega.Tauto.X_$a5,$adef_Coq.setoid_ring.Field_theory.almost_field_theory_$a10,$adef_Coq.Sorting.Sorted.Sorted_$a3,$adef_Coq.Init.Specif.sumor_$a2,$adef_Coq.micromega.RMicromega.CInv_$a1,$adef_Coq.PArith.BinPosDef.Pos.mul_$a2,$adef_$_lam_16626_$a2,$adef_Coq.PArith.BinPosDef.Pos.testbit_$a2,$adef_Coq.NArith.BinNatDef.N.mul_$a2,$adef_Coq.Init.Nat.pred_$a1,$adef_Coq.Lists.SetoidList.InA_$a2,$adef_$_prop_116345_$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_HList.hlist.Hcons_$a4,$adef_$_let_16_mkpow_28087_$a7,$adef_Coq.Lists.List.map_$a4,$adef_$_lam_2042_$a2,$adef_Coq.setoid_ring.Ring_polynom.Mphi_$a6,$adef_Coq.setoid_ring.Field_theory.NPEequiv_$a13,$adef_Coq.Init.Specif.inleft_$a3,$adef_Coq.micromega.EnvRing.Pinj_$a3,$adef_Coq.Init.Datatypes.cons_$a3,$adef_Coq.setoid_ring.Field_theory.field_theory_$a10,$adef_Coq.setoid_ring.Ring_theory.Computational_$a3,$adef_Coq.micromega.RingMicromega.PsatzSquare_$a2,$adef_ExtLib.Data.Member.to_nat_$a4,$adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1,$adef_Coq.Init.Datatypes.pair_$a4,$adef_Coq.ZArith.BinIntDef.Z.pred_double_$a1,$adef_$_let_18_mkmult_pow_28089_$a9,$adef_Coq.PArith.BinPosDef.Pos.IsPos_$a1,$adef_$_prop_116346_$a2,$adef_$_prop_34458_$a4,$adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a2,$adef_Coq.Lists.List.nth_ok_$a4,$adef_Coq.micromega.RingMicromega.Psatz_$a1,$adef_Coq.Init.Datatypes.Some_$a2,$adef_Coq.micromega.EnvRing.Pc_$a2,$adef_Coq.Structures.OrderedType.EQ_$a5,$adef_Coq.Lists.List.find_$a3,$adef_Coq.Numbers.BinNums.Zpos_$a1,$adef_Coq.Classes.RelationClasses.subrelation_$a3,$adef_Coq.Init.Datatypes.list_$a1,$adef_Coq.Init.Nat.sub_$a2,$adef_Coq.Lists.SetoidList.eqlistA_$a2,$adef_Coq.micromega.Tauto.clause_$a2,$adef_Coq.NArith.BinNatDef.N.add_$a2,$adef_Coq.ZArith.BinInt.Z.divide_$a2,$adef_Coq.Bool.Bool.ReflectF_$a1,$adef_Coq.setoid_ring.Ring_polynom.add_pow_list_$a4,$adef_Coq.QArith.QArith_base.Qinv_$a1,$adef_Coq.Reals.Rfunctions.ZintNull_$a1,$adef_Coq.Lists.List.removelast_$a2,$adef_Coq.micromega.EnvRing.PEX_$a2,$adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a11,$adef_Coq.setoid_ring.Field_theory.FEI_$a1,$adef_Coq.Bool.Bool.ReflectT_$a1,$adef_Coq.ZArith.Znumtheory.Euclid_$a2,$adef_Coq.Lists.List.nodup_$a3,$adef_HList.hlist.equiv_hlist_$a4,$adef_Coq.Lists.List.Forall_$a3,$adef_ExtLib.Tactics.Injection.result_$a2,$adef_Coq.QArith.QArith_base.Qplus_$a2,$adef_Coq.Lists.SetoidList.removeA_$a5,$adef_Coq.setoid_ring.Field_theory.Fcons00_$a11,$adef_Coq.setoid_ring.Field_theory.PExpr_eq_$a4,$adef_$_lam_34917_$a4,$adef_Coq.PArith.BinPosDef.Pos.sub_$a2,$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_$_lam_38194_$a3,$adef_Coq.ZArith.BinIntDef.Z.quotrem_$a2,$adef_$_lam_38202_$a4,$adef_Coq.micromega.RingMicromega.PsatzAdd_$a3,$adef_$_prop_46976_$a4,$adef_Coq.ZArith.BinIntDef.Z.min_$a2,$adef_$_lam_47646_$a6,$adef_Coq.micromega.Tauto.N_$a5,$adef_$_case_ExtLib.Data.Member.member$17801_$a4,$adef_$_prop_16914_$a3,$adef_Coq.setoid_ring.InitialRing.gen_phiN_$a6,$adef_Coq.Lists.SetoidList.equivlistA_$a4,$adef_$_prop_15770_$a3,$adef_Coq.Init.Nat.min_$a2,$adef_Coq.Init.Specif.existT2_$a6,$adef_Coq.micromega.RingMicromega.PsatzC_$a2,$adef_Coq.ZArith.BinInt.Zne_$a2,$adef_Coq.PArith.BinPosDef.Pos.compare_$a2,$adef_Coq.Lists.List.filter_$a3,$adef_Coq.ZArith.BinIntDef.Z.div_$a2,$adef_Coq.micromega.RingMicromega.PsatzZ_$a1,$adef_$_prop_34459_$a4,$adef_Coq.Bool.Bool.Is_true_$a1,$adef_$_fix_550_v_CANONICAL_1_$a3,$adef_Coq.Lists.List.nth_default_$a4,$adef_Coq.micromega.Tauto.eval_clause_$a6,$adef_Coq.Lists.List.fold_right_$a5,$adef_$_case_Coq.Init.Datatypes.list$17865_$a4,$adef_$_prop_116340_$a4,$adef_ExtLib.Tactics.Injection.Build_Injective_$a3,$adef_Coq.Lists.List.tl_$a2,$adef_$_lam_38202_$a3,$adef_Coq.setoid_ring.Ring_theory.sign_theory_$a4,$adef_$_case_Coq.Numbers.BinNums.Z$37861_$a2,$adef_$_lam_15512_$a2,$adef_Coq.setoid_ring.Field_theory.FEX_$a2,$adef_Coq.Lists.List.NoDup_$a2,$adef_Coq.Vectors.VectorDef.nil_$a1,$adef_Coq.Logic.EqdepFacts.Eq_rect_eq_on_$a4,$adef_Coq.Init.Specif.left_$a2,$adef_$_lam_15516_$a3,$adef_Coq.Init.Specif.sigT_$a2,$adef_Coq.micromega.RingMicromega.NFormula_$a1,$adef_Coq.ZArith.BinIntDef.Z.pow_$a2,$adef_$_lam_16646_$a5,$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_$_prop_16607_$a3,$adef_Coq.NArith.BinNatDef.N.eqb_$a2,$adef_Coq.NArith.BinNat.N.eqf_$a2,$adef_Coq.setoid_ring.Field_theory.denum_$a2,$adef_Coq.NArith.BinNat.N.le_$a2,$adef_Coq.Lists.List.incl_$a3,$adef_$_prop_37889_$a2,$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.QArith.QArith_base.Qopp_$a1,$adef_Coq.Init.Peano.gt_$a2,$tdef_$_type_36343,$tdef_$_type_46391,$tdef_$_type_35306,$tdef_$_type_11216,$tdef_$_type_23220,$tdef_$_type_1954,$tdef_$_type_41399,$tdef_$_type_42068,$tdef_$_type_19669,$tdef_$_type_7257,$tdef_$_type_6875,$tdef_$_type_69,$tdef_$_type_6868,$tdef_Coq.Init.Specif.sigT2,$tdef_$_type_46583,$tdef_$_type_36633,$tdef_$_type_45279,$tdef_$_type_37624,$tdef_$_type_37722,$tdef_$_type_19798,$tdef_$_type_46401,$tdef_$_type_29339,$tdef_Coq.Init.Datatypes.bool,$tdef_$_type_37627,$tdef_$_type_23083,$tdef_Coq.Structures.OrdersTac.ord,$tdef_Coq.micromega.EnvRing.PExpr,$tdef_$_type_24185,$tdef_$_type_18598,$tdef_$_type_33017,$tdef_$_type_2023,$tdef_$_type_41745,$tdef_$_type_34491,$tdef_$_type_17652,$tdef_$_type_37742,$tdef_$_type_11368,$tdef_$_type_18699,$tdef_$_type_47675,$tdef_$_type_113947,$tdef_Coq.Structures.OrderedTypeEx.N_as_OT.t,$tdef_$_type_35233,$tdef_$_type_35364,$tdef_$_type_121389,$tdef_$_type_24174,$tdef_$_type_37852,$tdef_$_type_121875,$tdef_$_type_9,$tdef_$_type_30039,$tdef_$_type_24194,$tdef_$_type_126706,$tdef_$_type_15311,$tdef_Coq.Init.Datatypes.comparison,$tdef_Coq.setoid_ring.Ring_polynom.Mon,$tdef_$_type_1907,$tdef_$_type_14698,$tdef_$_type_33067,$tdef_$_type_36141,$tdef_$_type_2522,$tdef_$_type_109,$tdef_$_type_29847,$tdef_$_type_45330,$tdef_$_type_35193,$tdef_Coq.micromega.Tauto.GFormula,$tdef_Coq.Init.Specif.sig2,$tdef_$_type_3139,$tdef_$_type_32803,$tdef_$_type_29817,$tdef_$_type_16632,$tdef_$_type_15670,$tdef_Coq.Init.Specif.sumbool,$tdef_$_type_34456,$tdef_$_type_17521,$tdef_$_type_5381,$tdef_$_type_19693,$tdef_$_type_18991,$tdef_$_type_2973,$tdef_$_type_46451,$tdef_$_type_17592,$tdef_$_type_34438,$tdef_$_type_5034,$tdef_$_type_29222,$tdef_$_type_29931,$tdef_$_type_35317,$tdef_Coq.setoid_ring.Field_theory.FExpr,$tdef_$_type_16614,$tdef_$_type_30012,$tdef_Coq.micromega.RMicromega.Rcst,$tdef_$_type_39000,$tdef_$_type_36615,$tdef_$_type_3146,$tdef_Coq.Init.Specif.sig,$tdef_Coq.Strings.Ascii.ascii,$tdef_$_type_33408,$tdef_$_type_19443,$tdef_Coq.Relations.Relation_Definitions.relation,$tdef_$_type_114199,$tdef_$_type_35420,$tdef_$_type_17185,$tdef_$_type_32967,$tdef_$_type_17692,$tdef_$_type_12444,$tdef_$_type_159686,$tdef_$_type_45389,$tdef_$_type_19434,$tdef_$_type_46580,$tdef_$_type_46515,$tdef_$_type_37757,$tdef_$_type_17419,$tdef_Coq.micromega.RingMicromega.Op2,$tdef_$_type_118488,$tdef_$_type_16735,$tdef_$_type_2379,$tdef_$_type_4998,$tdef_Coq.Init.Byte.byte,$tdef_$_type_37700,$tdef_$_type_39692,$tdef_$_type_2947,$tdef_Coq.Reals.Rfunctions.Z_spec,$tdef_$_type_33241,$tdef_$_type_38092,$tdef_$_type_1976,$tdef_Coq.ZArith.Zpower.Zdiv_rest_proofs,$tdef_Coq.Strings.String.string,$tdef_$_type_5068,$tdef_$_type_2286,$tdef_$_type_15657,$tdef_$_type_46627,$tdef_$_type_3103,$tdef_$_type_3064,$tdef_$_type_24199,$tdef_$_type_2554,$tdef_$_type_13682,$tdef_$_type_2671,$tdef_$_type_18076,$tdef_$_type_3068,$tdef_$_type_121139,$tdef_$_type_2143,$tdef_$_type_29684,$tdef_Coq.Init.Specif.sigT,$tdef_$_type_12789,$tdef_$_type_5092,$tdef_$_type_1966,$tdef_$_type_159798,$tdef_$_type_120501,$tdef_$_type_17562,$tdef_$_type_120510,$tdef_$_type_2174,$tdef_$_type_1914,$tdef_$_type_46547,$tdef_$_type_25373,$tdef_$_type_2628,$tdef_$_type_32373,$tdef_$_type_4143,$tdef_$_type_35588,$tdef_$_type_36706,$tdef_$_type_29553,$tdef_$_type_29276,$tdef_$_type_45285,$tdef_$_type_37761,$tdef_$_type_116538,$tdef_$_type_122692,$tdef_$_type_17645,$tdef_$_type_19437,$tdef_Coq.Structures.OrderedType.Compare,$tdef_Coq.Init.Specif.sumor,$tdef_$_type_46600,$tdef_$_type_99,$tdef_$_type_3153,$tdef_$_type_48333,$tdef_$_type_45172,$tdef_$_type_16770,$tdef_$_type_3218,$tdef_$_type_15477,$tdef_$_type_1912,$tdef_$_type_37593,$tdef_Coq.micromega.Tauto.cnf,$tdef_$_type_1926,$tdef_$_type_23156,$tdef_Coq.Numbers.BinNums.Z,$tdef_$_type_5123,$tdef_$_type_30492,$tdef_Coq.QArith.QArith_base.Q,$tdef_$_type_33109,$tdef_$_type_40361,$tdef_Coq.Numbers.BinNums.positive,$tdef_$_type_46488,$tdef_$_type_34711,$tdef_Coq.Init.Datatypes.nat,$tdef_$_type_33488,$tdef_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$tdef_$_type_724,$tdef_Coq.Init.Datatypes.prod,$tdef_$_type_7432,$tdef_$_type_38118,$tdef_$_type_31326,$tdef_Coq.micromega.RingMicromega.Formula,$tdef_$_type_4104,$tdef_$_type_36199,$tdef_$_type_27980,$tdef_$_type_11205,$tdef_$_type_17661,$tdef_$_type_1951,$tdef_$_type_2511,$tdef_$_type_21736,$tdef_$_type_87,$tdef_$_type_4436,$tdef_$_type_38366,$tdef_$_type_25658,$tdef_Coq.setoid_ring.Ring_theory.ring_kind,$tdef_$_type_36598,$tdef_Coq.micromega.Tauto.clause,$tdef_$_type_13781,$tdef_$_type_15488,$tdef_$_type_7164,$tdef_Coq.Vectors.VectorDef.t,$tdef_$_type_38100,$tdef_$_type_120279,$tdef_$_type_28,$tdef_$_type_37027,$tdef_$_type_44204,$tdef_$_type_2125,$tdef_$_type_646,$tdef_$_type_15621,$tdef_$_type_19666,$tdef_$_type_2177,$tdef_$_type_126742,$tdef_$_type_7339,$tdef_Coq.Vectors.Fin.t,$tdef_$_type_2968,$tdef_$_type_26565,$tdef_$_type_35280,$tdef_$_type_2035,$tdef_ExtLib.Core.RelDec.RelDec,$tdef_$_type_45240,$tdef_$_type_3876,$tdef_$_type_33536,$tdef_$_type_19193,$tdef_$_type_31965,$tdef_$_type_7071,$tdef_$_type_35336,$tdef_$_type_15505,$tdef_$_type_38450,$tdef_$_type_2118,$tdef_$_type_46603,$tdef_Coq.ZArith.Znumtheory.Euclid,$tdef_Coq.micromega.RingMicromega.Psatz,$tdef_$_type_7514,$tdef_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$tdef_$_type_20451,$tdef_$_type_7607,$tdef_iT,$tdef_$_type_38205,$tdef_ExtLib.Data.Member.member,$tdef_$_type_46459,$tdef_$_type_7748,$tdef_Coq.micromega.EnvRing.Mon,$tdef_$_type_3110,$tdef_$_type_2361,$tdef_$_type_29576,$tdef_$_type_17550,$tdef_$_type_31539,$tdef_$_type_2982,$tdef_$_type_43083,$tdef_$_type_12420,$tdef_$_type_15293,$tdef_$_type_118289,$tdef_$_type_4367,$tdef_$_type_3988,$tdef_$_type_38243,$tdef_ExtLib.Tactics.Injection.Injective,$tdef_$_type_2401,$tdef_$_type_2310,$tdef_Coq.Init.Datatypes.list,$tdef_$_type_46417,$tdef_$_type_13677,$tdef_$_type_46443,$tdef_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$tdef_$_type_34826,$tdef_$_type_28367,$tdef_$_type_29159,$tdef_Coq.Init.Datatypes.option,$tdef_$_type_15282,$tdef_$_type_16933,$tdef_$_type_37032,$tdef_$_type_29955,$tdef_$_type_17485,$tdef_$_type_33444,$tdef_$_type_114118,$tdef_$_type_37717,$tdef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$tdef_$_type_159676,$tdef_$_type_28821,$tdef_$_type_2211,$tdef_$_type_15497,$tdef_$_type_5063,$tdef_$_type_37724,$tdef_Coq.FSets.FSetPositive.PositiveSet.elt,$tdef_$_type_31113,$tdef_$_type_39346,$tdef_$_type_18800,$tdef_$_type_15345,$tdef_$_type_29599,$tdef_$_type_3945,$tdef_$_type_48237,$tdef_$_type_45243,$tdef_$_type_11239,$tdef_F,$tdef_$_type_23647,$tdef_$_type_36729,$tdef_$_type_42760,$tdef_$_type_36319,$tdef_Coq.Numbers.BinNums.N,$tdef_$_type_2071,$tdef_$_type_17451,$tdef_$_type_8672,$tdef_$_type_36170,$tdef_$_type_7969,$tdef_$_type_46686,$tdef_$_type_38089,$tdef_Coq.Reals.Rdefinitions.R,$tdef_$_type_46415,$tdef_$_type_2686,$tdef_Coq.micromega.ZMicromega.ZWitness,$tdef_$_type_37782,$tdef_$_type_114203,$tdef_$_type_46974,$tdef_$_type_16820,$tdef_$_type_2235,$tdef_$_type_2215,$tdef_$_type_32784,$tdef_$_type_2055,$tdef_$_type_122667,$tdef_$_type_11236,$tdef_Coq.micromega.ZMicromega.ZArithProof,$tdef_$_type_40707,$tdef_$_type_2952,$tdef_Coq.FSets.FSetPositive.PositiveSet.t,$tdef_$_type_35080,$tdef_$_type_35239,$tdef_$_type_17685,$tdef_Coq.Init.Datatypes.unit,$tdef_$_type_37617,$tdef_$_type_35115,$tdef_$_type_37914,$tdef_$_type_5009,$tdef_$_type_18130,$tdef_Coq.Init.Datatypes.sum,$tdef_$_type_45384,$tdef_$_type_3185,$tdef_$_type_20812,$tdef_$_type_35433,$tdef_$_type_13751,$tdef_$_type_2170,$tdef_$_type_2961,$tdef_Coq.FSets.FSetPositive.PositiveSet.tree,$tdef_$_type_35310,$tdef_$_type_1905,$tdef_$_type_72,$tdef_$_type_35216,$tdef_$_type_29988,$tdef_$_type_46478,$tdef_$_type_2684,$tdef_$_type_15709,$tdef_$_type_24177,$tdef_Coq.setoid_ring.Field_theory.linear,$tdef_$_type_28842,$tdef_Prop,$tdef_$_type_45001,$tdef_$_type_11311,$tdef_$_type_4063,$tdef_$_type_32817,$tdef_$_type_38095,$tdef_$_type_2194,$tdef_$_type_17771,$tdef_$_type_18890,$tdef_$_type_29666,$tdef_$_type_37596,$tdef_$_type_13160,$tdef_$_type_29096,$tdef_$_type_20962,$tdef_$_type_15781,$tdef_$_type_13125,$tdef_$_type_2218,$tdef_$_type_2663,$tdef_$_type_11157,$tdef_$_type_19752,$tdef_$_type_47653,$tdef_$_type_33500,$tdef_Coq.Classes.EquivDec.EqDec,$tdef_$_type_64,$tdef_Coq.Init.Datatypes.CompareSpecT,$tdef_Coq.micromega.RingMicromega.Op1,$tdef_$_type_15450,$tdef_$_type_38174,$tdef_$_type_17166,$tdef_$_type_15649,$tdef_$_type_126682,$tdef_$_type_37660,$tdef_Coq.setoid_ring.Field_theory.rsplit,$tdef_$_type_15433,$tdef_$_type_120240,$tdef_$_type_45258,$tdef_$_type_44,$tdef_Coq.micromega.EnvRing.Pol,$tdef_$_type_46490,$tdef_$_type_2357,$tdef_$_type_7767,$tdef_$_type_15387,$tdef_$_type_32160,$tdef_$_type_38186,$tdef_$_type_34861,$tdef_$_type_120259,$tdef_$_type_126485,$tdef_$_type_116455,$tdef_$_type_15463,$tdef_$_type_5080,$tdef_$_type_36623,$tdef_$_type_121764,$tdef_$_type_34447,$tdef_$_type_30705,$tdef_$_type_40015,$tdef_Coq.Bool.Bool.reflect,$tdef_$_type_2153,$tdef_Coq.setoid_ring.Ring_polynom.Pol,$tdef_$_type_33790,$tdef_$_type_2001,$tdef_$_type_29640,$tdef_$_type_5024,$tdef_$_type_45164,$tdef_$_type_45156,$tdef_$_type_2699,$tdef_$_type_38109,$tdef_$_type_46406,$tdef_$_type_220,$tdef_$_type_46531,$tdef_$_type_38179,$tdef_$_type_37702,$tdef_$_type_34479,$tdef_$_type_118673,$tdef_$_type_33708,$tdef_$_type_46666,$tdef_$_type_37581,$tdef_$_type_30918,$tdef_HList.hlist.hlist,$tdef_$_type_34907,$tdef_$_type_9700,$tdef_$_type_4129,$tdef_$_type_37785,$tdef_$_type_29622,$tdef_$_type_29871,$tdef_$_type_19092,$tdef_$_type_16977,$tdef_$_type_35359,$tdef_$_type_13903,$tdef_$_type_35376,$tdef_Coq.setoid_ring.Ring_polynom.PExpr,$tdef_Coq.micromega.RingMicromega.PolC,$tdef_$_type_121639,$tdef_$_type_33364,$tdef_$_type_3288,$tdef_$_type_41053,$tdef_$_type_4114,$tdef_$_type_43752,$tdef_$_type_15309,$tdef_$_type_2445,$tdef_$_type_32568,$tdef_$_type_35414,$tdef_$_type_20807,$tdef_$_type_31752,$tdef_$_type_35187,$tdef_$_type_120588,$tdef_Coq.Sets.Relations_1.Relation,$tdef_$_type_2533,$tdef_$_type_35252,$tdef_$_type_24180,$tdef_$_type_1217,$tdef_Type,$tdef_$_type_121514,$tdef_Coq.PArith.BinPosDef.Pos.mask,$tdef_$_type_5011,$tdef_$_type_35210,$tdef_Coq.micromega.RingMicromega.NFormula,$tdef_$_type_19675,$tdef_$_type_35275,$tdef_$_type_35324,$tdef_$_type_25119,$tdef_$_type_38465,$tdef_$_type_33834,$tdef_$_type_3166,$tdef_$_type_2434,$tdef_$_type_46480,$tdef_$_type_2,$tdef_$_type_16605,$tdef_$_type_46987,$tdef_$_type_33159,$tdef_$_type_121264,$tdef_Coq.setoid_ring.InitialRing.Nword,$tdef_$_type_42414,$tdef_$_type_3259,$tdef_$_type_29901,$tdef_$_type_3262,$tdef_$_type_43406,$tdef_$_type_122416,$tdef_$_type_20820] % 31.62/31.48 =============================================================== % 31.62/31.48 % 31.62/31.48 Combined formula: 3117 axiom(s) => conjecture % 31.62/31.48 % 31.62/31.48 % Equality/functions detected -> nanoCoP oracle mode % 31.62/31.48 nanoCoP : % 31.62/31.48 % 23,830,042 inferences, 26.866 CPU in 26.878 seconds (100% CPU, 887006 Lips) % 31.62/31.48 % 31.62/31.48 % nanoCoP proof (equality/functions) % 31.62/31.48 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 31.62/31.48 % 31.62/31.48 % SZS output end Proof %------------------------------------------------------------------------------