# 
# CANDIDATI
# =========
# 
# 500	
#
cic:/Coq/Reals/Rgeom/isometric_rotation.con.body
cic:/CoRN/reals/IVT/b_mon'.con.body
cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con.body
# 
# 1000
#
cic:/Rocq/TreeAutomata/lattice_fixpoint/map_maxi_maxi.con.body
cic:/Sophia-Antipolis/Float/FroundPlus/radixRangeBoundExp_subproof5.con.body
cic:/Sophia-Antipolis/Float/FroundPlus/radixRangeBoundExp_subproof0.con.body
# 
# 1500
# 
cic:/Sophia-Antipolis/MATHS/GROUPS/g2/T4R1.con.body
cic:/Coq/Reals/RList/RList_P15.con.body
cic:/Rocq/THREE_GAP/Nat_compl/ge_trans.con.body
# 
# 2000
# 
cic:/Sophia-Antipolis/Algebra/Parts2/compl_comp_rev.con.body
cic:/Cachan/SMC/make/BDDmake_node_height_le.con.body
cic:/Orsay/ExactRealArithmetic/Zsqrt_complements/Zsqrt_sqrt_bis.con.body
# 
# 2500
# 
cic:/Eindhoven/POCKLINGTON/modprime/techlemma3.con.body
cic:/Sophia-Antipolis/Cours-de-Coq/Fil/Pairs_are_enough_finite_case.con.body
cic:/Nijmegen/QArith/Qquadratic_sign/Qquadratic_sign_One_y.con.body
# 
# 3000
# 
cic:/CoRN/ftc/Integral/partition_join_aux'.con.body
cic:/Sophia-Antipolis/geometry/reflexion_plane/reflexion_projete_orthogonal_milieu.con.body
cic:/Sophia-Antipolis/geometry/trigo/trigo_Pythagore.con.body
# 
# 3500
# 
cic:/CoRN/algebra/CPolynomials/nexp_apply.con.body
cic:/Sophia-Antipolis/Angles/point_cocyclicite/reciproque_cocyclique.con.body
cic:/Coq/Reals/Rtrigo/sin_increasing_0.con.body
# 
# 4000
# 
cic:/CoRN/algebra/CAbGroups/nmult_plus'.con.body
cic:/CoRN/fta/KeyLemma/lem_1a.con.body
cic:/Coq/Reals/Exp_prop/exp_form.con.body
# 
# 4500
# 
cic:/Utrecht/ABP/abp_lem1/CommLs5.con.body
cic:/CoRN/complex/NRootCC/nrCC4_a1.con.body
cic:/Coq/Reals/Rpower/ln_continue.con.body
# 
# 5000
# 
cic:/Sophia-Antipolis/geometry/barycentre/unicite_coor_bar.con.body
cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con.body
cic:/CoRN/algebra/CRings/nring_different.con.body
# 
# 5500
# 
cic:/Sophia-Antipolis/geometry/milieu/milieu_distinct2.con.body
cic:/Utrecht/ABP/abp_proc/LemLin3.con.body
cic:/Utrecht/ABP/abp_proc/LemLin6.con.body
# 
# 6000
# 
cic:/Montevideo/FSSecModel/chownIsSecure/ChownPSP.con.body
cic:/Sophia-Antipolis/Bertrand/Knuth_why/Prime_po_9_subproof46.con.body
cic:/Montevideo/FSSecModel/chmodIsSecure/ChmodPSP.con.body
# 
# 6500
# 
cic:/CoRN/fta/CC_Props/seq_yields_zero.con.body
cic:/Sophia-Antipolis/Bertrand/Knuth_why/Prime_po_9_subproof58.con.body
cic:/Nijmegen/QArith/Qpositive_sub/le_minus_left_subproof.con.body
# 
# 7000
# 
cic:/Nijmegen/QArith/Qpositive_sub/Qpositive_sub_correct.con.body
cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con.body
cic:/Cachan/SMC/config/bs_node_height_right.con.body
# 
# 7500
# 
cic:/Sophia-Antipolis/Huffman/PBTree2BTree/to_btree_inb.con.body
cic:/CoRN/reals/Series/ratio_test_div.con.body
cic:/Sophia-Antipolis/Buchberger/Pminus/minusP_inv3b.con.body
# 
# 8000
# 
cic:/Rocq/COC/Termes/mem_sort_subst.con.body
cic:/Sophia-Antipolis/geometry/orthocentre/deux_hauteurs_trois.con.body
cic:/Rocq/GRAPHS/cgraph/ad_1_path_dist_big_enough_1.con.body
# 
# 8500
# 
cic:/CoRN/reals/Series/aew_series_conv.con.body
cic:/Nijmegen/QArith/homographicAcc_Qhomographic_sign/Qhomographic_Qpositive_to_Q_homographicAcc_pos_1.con.body
cic:/Sophia-Antipolis/Buchberger/Pspoly/fconfl_top.con.body
# 
# 9000
# 
cic:/Coq/Reals/Ranalysis2/maj_term3.con.body
cic:/Sophia-Antipolis/geometry/representant_unitaire/unicite_representant_unitaire.con.body
cic:/Sophia-Antipolis/MATHS/DOMAINS/triple/Triples_are_enough_finite_case.con.body
# 
# 9500
# 
cic:/CoRN/reals/CauchySeq/str_Archimedes.con.body
cic:/Coq/romega/ReflOmegaCore/T_OMEGA13_stable.con.body
cic:/Orsay/Maths/divide/divide_1.con.body
# 
# 10000
# 
cic:/Nijmegen/QArith/general_Q/Qpositive_c_equal_subproof1.con.body
cic:/Rocq/TreeAutomata/inter_correct/preDTA_produit_l_ref_ok.con.body
cic:/Rocq/AILS/ails/step2.con.body
# 
# 20000
# 
cic:/Sophia-Antipolis/geometry/mesure_algebrique/barycentre_mes_alg.con.body
cic:/Coq/Reals/Ranalysis1/deriv_maximum.con.body
cic:/CoRN/ftc/Integral/integral_empty.con.body
# 
# 30000
# 
cic:/CoRN/reals/iso_CReals/less_pres_Lim.con.body
cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_plus.con.body
cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con.body
# 
# 40000
# 
cic:/Nijmegen/QArith/Qquadratic_Qpositive_to_Q_properties/Qquadratic_Qpositive_to_Q_0_subproof.con.body
cic:/Sophia-Antipolis/geometry/barycentre/unicite_coor_bar_aux.con.body
cic:/CoRN/algebra/COrdCauchy/CS_seq_mult.con.body
# 
# 50000
# 
cic:/CoRN/transc/Pi/pi_seq_Cauchy.con.body
cic:/Rocq/TreeAutomata/inter/predta_produit_5.con.body
cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con.body
# 
# 60000
# 
cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con.body
cic:/Orsay/ExactRealArithmetic/Lemmes_generaux/Zsqr_cond.con.body
cic:/Rocq/COMPILER/Mini_ML/ML_DS_determ.con.body
# 
# 70000
# 
cic:/CoRN/reals/IVT/intervals_small''.con.body
cic:/Sophia-Antipolis/geometry/Plans_paralleles/para_plan_sym.con.body
cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con.body
# 
# 80000
# 
cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist_n.con.body
cic:/Nijmegen/QArith/Qquadratic_Qpositive_to_Qpositive/Qquadratic_Qpositive_to_Qpositive_equal.con.body
cic:/Sophia-Antipolis/geometry/Droite_plan_espace/points_plan_espace.con.body
# 
# 90000
# 
cic:/Sophia-Antipolis/Bertrand/Knuth_why/Prime_po_9.con.body
cic:/CoRN/transc/InvTrigonom/Tan_ilim.con.body
cic:/Nijmegen/QArith/Qquadratic_Qpositive_to_Q_properties/Qquadratic_Qpositive_to_Q_4_subproof.con.body
# 
# 100000
# 
cic:/CoRN/tactics/GroupReflection/MM_plus_corr_G.con.body
cic:/Nijmegen/QArith/Qquadratic_Qpositive_to_Q_properties/Qquadratic_Qpositive_to_Q_5_subproof.con.body
cic:/Rocq/DEMOS/Demo_AutoRewrite/ResAck0.con.body
# 
# 200000
# 
cic:/CoRN/ftc/Composition/Derivative_I_comp.con.body
cic:/CoRN/metrics/Equiv/inv_isopsmetry.con.body
cic:/Cachan/SMC/mu/mu_eval_lemma2.con.body
#
# A NOI CARI
# ==========
# 
# 7211	cic:/Coq/Reals/Rlimit/limit_inv.con.body
# 3054	cic:/Coq/Reals/Rlimit/limit_mul.con.body
# 1172	cic:/Coq/Reals/Rlimit/limit_plus.con.body
#