-cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
-cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
-cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
-cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
-cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/appA.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
-cic:/matita/algebra/CoRN/SetoidFun/UR.con
-cic:/matita/algebra/CoRN/SetoidFun/UQ.con
-cic:/matita/algebra/CoRN/SetoidFun/UP.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
-cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
-cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
-cic:/matita/algebra/CoRN/SetoidFun/Inv.con
-cic:/matita/algebra/CoRN/SetoidFun/Fid.con
-cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
-cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
-cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
-cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
-cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
-cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
-cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
-cic:/matita/algebra/CoRN/SetoidFun/BR.con
-cic:/matita/algebra/CoRN/SetoidFun/BQ.con
-cic:/matita/algebra/CoRN/SetoidFun/BP.con
-cic:/matita/algebra/CoRN/SetoidFun/Astar.con
-cic:/matita/demo/realisability/correct2.con
-cic:/matita/demo/realisability/correct.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
-cic:/matita/demo/realisability/type_OF_SP.con
-cic:/matita/demo/realisability/true_impl_realized.con
-cic:/matita/demo/realisability/sigma_rect.con
-cic:/matita/demo/realisability/sigma_rec.con
-cic:/matita/demo/realisability/sigma_ind.con
-cic:/matita/demo/realisability/sigma.ind
-cic:/matita/demo/realisability/realized.con
-cic:/matita/demo/realisability/pi2.con
-cic:/matita/demo/realisability/pi1.con
-cic:/matita/demo/realisability/modr.con
-cic:/matita/demo/realisability/id_axiom.con
-cic:/matita/demo/realisability/extraction.con
-cic:/matita/demo/realisability/elim_abs.con
-cic:/matita/demo/realisability/cut.con
-cic:/matita/demo/realisability/and_i.con
-cic:/matita/demo/realisability/SP_rect.con
-cic:/matita/demo/realisability/SP_rec.con
-cic:/matita/demo/realisability/SP_ind.con
-cic:/matita/demo/realisability/SP.ind
-cic:/matita/demo/realisability/Prop_OF_SP.con
cic:/matita/Q/Qaxioms/symmetric_Qtimes.con
cic:/matita/Q/Qaxioms/symmetric_Qplus.con
cic:/matita/Q/Qaxioms/sigma_Q.con
cic:/matita/Z/z/Z.ind
cic:/matita/Z/z/OZ_test_to_Prop.con
cic:/matita/Z/z/OZ_test.con
-cic:/matita/datatypes/bool/true_to_true_to_andb_true.con
-cic:/matita/datatypes/bool/orb_sym.con
-cic:/matita/datatypes/bool/orb_elim.con
-cic:/matita/datatypes/bool/orb.con
-cic:/matita/datatypes/bool/notb_notb.con
-cic:/matita/datatypes/bool/notb_elim.con
-cic:/matita/datatypes/bool/notb.con
-cic:/matita/datatypes/bool/not_eq_true_false.con
-cic:/matita/datatypes/bool/injective_notb.con
-cic:/matita/datatypes/bool/if_then_else.con
-cic:/matita/datatypes/bool/bool_to_decidable_eq.con
-cic:/matita/datatypes/bool/bool_rect.con
-cic:/matita/datatypes/bool/bool_rec.con
-cic:/matita/datatypes/bool/bool_ind.con
-cic:/matita/datatypes/bool/bool_elim.con
-cic:/matita/datatypes/bool/bool.ind
-cic:/matita/datatypes/bool/andb_true_true_r.con
-cic:/matita/datatypes/bool/andb_true_true.con
-cic:/matita/datatypes/bool/andb_sym.con
-cic:/matita/datatypes/bool/andb_elim.con
-cic:/matita/datatypes/bool/andb_assoc.con
-cic:/matita/datatypes/bool/andb.con
-cic:/matita/datatypes/bool/and_true.con
-cic:/matita/datatypes/bool/P_x_to_P_x_to_eq.con
-cic:/matita/datatypes/compare/compare_rect.con
-cic:/matita/datatypes/compare/compare_rec.con
-cic:/matita/datatypes/compare/compare_invert.con
-cic:/matita/datatypes/compare/compare_ind.con
-cic:/matita/datatypes/compare/compare.ind
-cic:/matita/datatypes/constructors/void_rect.con
-cic:/matita/datatypes/constructors/void_rec.con
-cic:/matita/datatypes/constructors/void_ind.con
-cic:/matita/datatypes/constructors/void.ind
-cic:/matita/datatypes/constructors/unit_rect.con
-cic:/matita/datatypes/constructors/unit_rec.con
-cic:/matita/datatypes/constructors/unit_ind.con
-cic:/matita/datatypes/constructors/unit.ind
-cic:/matita/datatypes/constructors/snd.con
-cic:/matita/datatypes/constructors/option_rect.con
-cic:/matita/datatypes/constructors/option_rec.con
-cic:/matita/datatypes/constructors/option_ind.con
-cic:/matita/datatypes/constructors/option.ind
-cic:/matita/datatypes/constructors/fst.con
-cic:/matita/datatypes/constructors/eq_pair_fst_snd.con
-cic:/matita/datatypes/constructors/Sum_rect.con
-cic:/matita/datatypes/constructors/Sum_rec.con
-cic:/matita/datatypes/constructors/Sum_ind.con
-cic:/matita/datatypes/constructors/Sum.ind
-cic:/matita/datatypes/constructors/Prod_rect.con
-cic:/matita/datatypes/constructors/Prod_rec.con
-cic:/matita/datatypes/constructors/Prod_ind.con
-cic:/matita/datatypes/constructors/Prod.ind
-cic:/matita/decidable_kit/decidable/reflect_rect.con
-cic:/matita/decidable_kit/decidable/reflect_rec.con
-cic:/matita/decidable_kit/decidable/reflect_inv.con
-cic:/matita/decidable_kit/decidable/reflect_ind.con
-cic:/matita/decidable_kit/decidable/reflect.ind
-cic:/matita/decidable_kit/decidable/prove_reflect.con
-cic:/matita/decidable_kit/decidable/p2bT.con
-cic:/matita/decidable_kit/decidable/p2bF.con
-cic:/matita/decidable_kit/decidable/orbP.con
-cic:/matita/decidable_kit/decidable/orbC.con
-cic:/matita/decidable_kit/decidable/orb.con
-cic:/matita/decidable_kit/decidable/negbP.con
-cic:/matita/decidable_kit/decidable/negb.con
-cic:/matita/decidable_kit/decidable/ltb_refl.con
-cic:/matita/decidable_kit/decidable/ltb_n_Sm.con
-cic:/matita/decidable_kit/decidable/ltbW.con
-cic:/matita/decidable_kit/decidable/ltbP.con
-cic:/matita/decidable_kit/decidable/ltb.con
-cic:/matita/decidable_kit/decidable/ltW.con
-cic:/matita/decidable_kit/decidable/ltS.con
-cic:/matita/decidable_kit/decidable/ltS'.con
-cic:/matita/decidable_kit/decidable/leb_refl.con
-cic:/matita/decidable_kit/decidable/leb_eqb.con
-cic:/matita/decidable_kit/decidable/lebW.con
-cic:/matita/decidable_kit/decidable/lebP.con
-cic:/matita/decidable_kit/decidable/idP.con
-cic:/matita/decidable_kit/decidable/eq_to_bool.con
-cic:/matita/decidable_kit/decidable/congr_S.con
-cic:/matita/decidable_kit/decidable/bool_to_eq.con
-cic:/matita/decidable_kit/decidable/b2pT.con
-cic:/matita/decidable_kit/decidable/b2pF.con
-cic:/matita/decidable_kit/decidable/andbPF.con
-cic:/matita/decidable_kit/decidable/andbP.con
-cic:/matita/decidable_kit/decidable/andb.con
-cic:/matita/decidable_kit/eqtype/test_canonical_option_eqType.con
-cic:/matita/decidable_kit/eqtype/sval.con
-cic:/matita/decidable_kit/eqtype/sub_eqType.con
-cic:/matita/decidable_kit/eqtype/sprop.con
-cic:/matita/decidable_kit/eqtype/sort_OF_nat.con
-cic:/matita/decidable_kit/eqtype/sort_OF_bool.con
-cic:/matita/decidable_kit/eqtype/sort.con
-cic:/matita/decidable_kit/eqtype/sigma_rect.con
-cic:/matita/decidable_kit/eqtype/sigma_rec.con
-cic:/matita/decidable_kit/eqtype/sigma_ind.con
-cic:/matita/decidable_kit/eqtype/sigma_eq_dec.con
-cic:/matita/decidable_kit/eqtype/sigma.ind
-cic:/matita/decidable_kit/eqtype/option_eqType.con
-cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con
-cic:/matita/decidable_kit/eqtype/ocmpP.con
-cic:/matita/decidable_kit/eqtype/ocmp.con
-cic:/matita/decidable_kit/eqtype/nat_eqType.con
-cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con
-cic:/matita/decidable_kit/eqtype/in_sub_rect.con
-cic:/matita/decidable_kit/eqtype/in_sub_rec.con
-cic:/matita/decidable_kit/eqtype/in_sub_inv.con
-cic:/matita/decidable_kit/eqtype/in_sub_ind.con
-cic:/matita/decidable_kit/eqtype/in_sub_eq.con
-cic:/matita/decidable_kit/eqtype/in_sub.ind
-cic:/matita/decidable_kit/eqtype/if_p.con
-cic:/matita/decidable_kit/eqtype/eqbP.con
-cic:/matita/decidable_kit/eqtype/eq_compatible.con
-cic:/matita/decidable_kit/eqtype/eqType_rect.con
-cic:/matita/decidable_kit/eqtype/eqType_rec.con
-cic:/matita/decidable_kit/eqtype/eqType_ind.con
-cic:/matita/decidable_kit/eqtype/eqType_decidable.con
-cic:/matita/decidable_kit/eqtype/eqType.ind
-cic:/matita/decidable_kit/eqtype/eqP.con
-cic:/matita/decidable_kit/eqtype/cmp_refl.con
-cic:/matita/decidable_kit/eqtype/cmpP.con
-cic:/matita/decidable_kit/eqtype/cmpC.con
-cic:/matita/decidable_kit/eqtype/cmp.con
-cic:/matita/decidable_kit/eqtype/bool_eqType.con
-cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con
-cic:/matita/decidable_kit/eqtype/bcmpP.con
-cic:/matita/decidable_kit/eqtype/bcmp.con
-cic:/matita/decidable_kit/fgraph/uniq_infgraphseq.con
-cic:/matita/decidable_kit/fgraph/setA.con
-cic:/matita/decidable_kit/fgraph/orb_refl.con
-cic:/matita/decidable_kit/fgraph/multss.con
-cic:/matita/decidable_kit/fgraph/multes.con
-cic:/matita/decidable_kit/fgraph/mkpermr.con
-cic:/matita/decidable_kit/fgraph/mem_multss.con
-cic:/matita/decidable_kit/fgraph/mem_multes.con
-cic:/matita/decidable_kit/fgraph/mem_mkpermr_size.con
-cic:/matita/decidable_kit/fgraph/mem_infgraphseq.con
-cic:/matita/decidable_kit/fgraph/mem_concat.con
-cic:/matita/decidable_kit/fgraph/iter.con
-cic:/matita/decidable_kit/fgraph/infgraphseq.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_rect.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_rec.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_inv.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_ind.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec.ind
-cic:/matita/decidable_kit/fgraph/infgraphP.con
-cic:/matita/decidable_kit/fgraph/infgraph.con
-cic:/matita/decidable_kit/fgraph/fval_eqE.con
-cic:/matita/decidable_kit/fgraph/fval.con
-cic:/matita/decidable_kit/fgraph/fproof.con
-cic:/matita/decidable_kit/fgraph/fgraph_eqType.con
-cic:/matita/decidable_kit/fgraph/fgraph_eqP.con
-cic:/matita/decidable_kit/fgraph/fgraph_default.con
-cic:/matita/decidable_kit/fgraph/fgraphType_rect.con
-cic:/matita/decidable_kit/fgraph/fgraphType_rec.con
-cic:/matita/decidable_kit/fgraph/fgraphType_ind.con
-cic:/matita/decidable_kit/fgraph/fgraphType.ind
-cic:/matita/decidable_kit/fgraph/count_setA.con
-cic:/matita/decidable_kit/fintype/uniq_tail.con
-cic:/matita/decidable_kit/fintype/uniq_mem.con
-cic:/matita/decidable_kit/fintype/uniq_fintype_enum.con
-cic:/matita/decidable_kit/fintype/uniqP.con
-cic:/matita/decidable_kit/fintype/uniq.con
-cic:/matita/decidable_kit/fintype/sub_finType.con
-cic:/matita/decidable_kit/fintype/sub_enumP.con
-cic:/matita/decidable_kit/fintype/segment_finType.con
-cic:/matita/decidable_kit/fintype/segment_enum.con
-cic:/matita/decidable_kit/fintype/segment.con
-cic:/matita/decidable_kit/fintype/mem_finType.con
-cic:/matita/decidable_kit/fintype/mem_filter.con
-cic:/matita/decidable_kit/fintype/is_some.con
-cic:/matita/decidable_kit/fintype/iota_ltb.con
-cic:/matita/decidable_kit/fintype/fsort.con
-cic:/matita/decidable_kit/fintype/finType_rect.con
-cic:/matita/decidable_kit/fintype/finType_rec.con
-cic:/matita/decidable_kit/fintype/finType_ind.con
-cic:/matita/decidable_kit/fintype/finType.ind
-cic:/matita/decidable_kit/fintype/filter.con
-cic:/matita/decidable_kit/fintype/enum_uniq.con
-cic:/matita/decidable_kit/fintype/enum.con
-cic:/matita/decidable_kit/fintype/count_O_mem.con
-cic:/matita/decidable_kit/fintype/count_O.con
-cic:/matita/decidable_kit/fintype/andbC.con
-cic:/matita/decidable_kit/fintype/andbA.con
-cic:/matita/decidable_kit/fintype/Type_OF_finType.con
-cic:/matita/decidable_kit/list_aux/mem.con
-cic:/matita/decidable_kit/list_aux/list_eqType.con
-cic:/matita/decidable_kit/list_aux/lcmp_length.con
-cic:/matita/decidable_kit/list_aux/lcmpP.con
-cic:/matita/decidable_kit/list_aux/lcmp.con
-cic:/matita/decidable_kit/list_aux/count.con
-cic:/matita/decidable_kit/streicher/stepH.con
-cic:/matita/decidable_kit/streicher/step.con
-cic:/matita/decidable_kit/streicher/pirrel.con
-cic:/matita/decidable_kit/streicher/nu_k.con
-cic:/matita/decidable_kit/streicher/nu_inv.con
-cic:/matita/decidable_kit/streicher/nu.con
-cic:/matita/decidable_kit/streicher/decT.con
-cic:/matita/decidable_kit/streicher/cancel_nu_nu_inv.con
-cic:/matita/decidable_kit/streicher/cancel.con
-cic:/matita/higher_order_defs/functions/symmetric2.con
-cic:/matita/higher_order_defs/functions/symmetric.con
-cic:/matita/higher_order_defs/functions/surjective.con
-cic:/matita/higher_order_defs/functions/monotonic.con
-cic:/matita/higher_order_defs/functions/injective.con
-cic:/matita/higher_order_defs/functions/eq_f_g_h.con
-cic:/matita/higher_order_defs/functions/distributive2.con
-cic:/matita/higher_order_defs/functions/distributive.con
-cic:/matita/higher_order_defs/functions/compose.con
-cic:/matita/higher_order_defs/functions/associative.con
-cic:/matita/higher_order_defs/ordering/antisymmetric.con
-cic:/matita/higher_order_defs/relations/transitive.con
-cic:/matita/higher_order_defs/relations/tight_apart.con
-cic:/matita/higher_order_defs/relations/symmetric.con
-cic:/matita/higher_order_defs/relations/relation.con
-cic:/matita/higher_order_defs/relations/reflexive.con
-cic:/matita/higher_order_defs/relations/irreflexive.con
-cic:/matita/higher_order_defs/relations/cotransitive.con
-cic:/matita/higher_order_defs/relations/antisymmetric.con
-cic:/matita/list/in/not_in_list_nil.con
-cic:/matita/list/in/mem_true_to_in_list.con
-cic:/matita/list/in/mem.con
-cic:/matita/list/in/incl_A_A.con
-cic:/matita/list/in/incl.con
-cic:/matita/list/in/in_list_to_mem_true.con
-cic:/matita/list/in/in_list_to_in_list_append_r.con
-cic:/matita/list/in/in_list_to_in_list_append_l.con
-cic:/matita/list/in/in_list_tail.con
-cic:/matita/list/in/in_list_singleton_to_eq.con
-cic:/matita/list/in/in_list_inv.con
-cic:/matita/list/in/in_list_ind.con
-cic:/matita/list/in/in_list_filter_to_p_true.con
-cic:/matita/list/in/in_list_filter_r.con
-cic:/matita/list/in/in_list_filter.con
-cic:/matita/list/in/in_list_cons_case.con
-cic:/matita/list/in/in_list_append_to_or_in_list.con
-cic:/matita/list/in/in_list.ind
-cic:/matita/list/list/x3.con
-cic:/matita/list/list/x2.con
-cic:/matita/list/list/x1.con
-cic:/matita/list/list/tmp.con
-cic:/matita/list/list/tail.con
-cic:/matita/list/list/permutation_inv.con
-cic:/matita/list/list/permutation_ind.con
-cic:/matita/list/list/permutation.ind
-cic:/matita/list/list/permut1_inv.con
-cic:/matita/list/list/permut1_ind.con
-cic:/matita/list/list/nth.con
-cic:/matita/list/list/nil_cons.con
-cic:/matita/list/list/map.con
-cic:/matita/list/list/list_rect.con
-cic:/matita/list/list/list_rec.con
-cic:/matita/list/list/list_ind2.con
-cic:/matita/list/list/list_ind.con
-cic:/matita/list/list/list.ind
-cic:/matita/list/list/length.con
-cic:/matita/list/list/le_length_filter.con
-cic:/matita/list/list/iota.con
-cic:/matita/list/list/id_list.con
-cic:/matita/list/list/foldr.con
-cic:/matita/list/list/filter.con
-cic:/matita/list/list/eq_map.con
-cic:/matita/list/list/cons_append_commute.con
-cic:/matita/list/list/associative_append.con
-cic:/matita/list/list/append_nil.con
-cic:/matita/list/list/append_cons.con
-cic:/matita/list/list/append.con
-cic:/matita/list/sort/sorted_to_minimum.con
-cic:/matita/list/sort/sorted_to_eq_sorted_b_true.con
-cic:/matita/list/sort/sorted_inv.con
-cic:/matita/list/sort/sorted_ind.con
-cic:/matita/list/sort/sorted_cons_to_sorted.con
-cic:/matita/list/sort/sorted.ind
-cic:/matita/list/sort/ordered_injective.con
-cic:/matita/list/sort/ordered.con
-cic:/matita/list/sort/insertionsort_sorted.con
-cic:/matita/list/sort/insertionsort.con
-cic:/matita/list/sort/insert_sorted.con
-cic:/matita/list/sort/insert_ind.con
-cic:/matita/list/sort/insert.con
-cic:/matita/logic/coimplication/iff_trans.con
-cic:/matita/logic/coimplication/iff_sym.con
-cic:/matita/logic/coimplication/iff_refl.con
-cic:/matita/logic/coimplication/iff_intro.con
-cic:/matita/logic/coimplication/Iff.con
-cic:/matita/logic/connectives/proj2.con
-cic:/matita/logic/connectives/proj1.con
-cic:/matita/logic/connectives/iff.con
-cic:/matita/logic/connectives/ex_ind.con
-cic:/matita/logic/connectives/ex2_ind.con
-cic:/matita/logic/connectives/ex2.ind
-cic:/matita/logic/connectives/ex.ind
-cic:/matita/logic/connectives/decidable.con
-cic:/matita/logic/connectives/absurd.con
-cic:/matita/logic/connectives/True_rect.con
-cic:/matita/logic/connectives/True_rec.con
-cic:/matita/logic/connectives/True_ind.con
-cic:/matita/logic/connectives/True.ind
-cic:/matita/logic/connectives/Or_ind.con
-cic:/matita/logic/connectives/Or_ind'.con
-cic:/matita/logic/connectives/Or.ind
-cic:/matita/logic/connectives/Not.con
-cic:/matita/logic/connectives/False_rect.con
-cic:/matita/logic/connectives/False_rec.con
-cic:/matita/logic/connectives/False_ind.con
-cic:/matita/logic/connectives/False.ind
-cic:/matita/logic/connectives/And_rect.con
-cic:/matita/logic/connectives/And_rec.con
-cic:/matita/logic/connectives/And_ind.con
-cic:/matita/logic/connectives/And.ind
-cic:/matita/logic/connectives2/transitive_iff.con
-cic:/matita/logic/connectives2/symmetric_iff.con
-cic:/matita/logic/connectives2/reflexive_iff.con
-cic:/matita/logic/equality/transitive_eq.con
-cic:/matita/logic/equality/trans_sym_eq.con
-cic:/matita/logic/equality/trans_eq.con
-cic:/matita/logic/equality/symmetric_eq.con
-cic:/matita/logic/equality/sym_eq.con
-cic:/matita/logic/equality/reflexive_eq.con
-cic:/matita/logic/equality/nu_left_inv.con
-cic:/matita/logic/equality/nu_inv.con
-cic:/matita/logic/equality/nu_constant.con
-cic:/matita/logic/equality/nu.con
-cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con
-cic:/matita/logic/equality/eq_rect.con
-cic:/matita/logic/equality/eq_rect'.con
-cic:/matita/logic/equality/eq_rec.con
-cic:/matita/logic/equality/eq_ind.con
-cic:/matita/logic/equality/eq_f2.con
-cic:/matita/logic/equality/eq_f.con
-cic:/matita/logic/equality/eq_f'.con
-cic:/matita/logic/equality/eq_elim_r.con
-cic:/matita/logic/equality/eq_elim_r'.con
-cic:/matita/logic/equality/eq_elim_r''.con
-cic:/matita/logic/equality/eq_OF_eq2.con
-cic:/matita/logic/equality/eq_OF_eq1.con
-cic:/matita/logic/equality/eq_OF_eq.con
-cic:/matita/logic/equality/eq.ind
-cic:/matita/logic/equality/comp.con
-cic:/matita/nat/bertrand/tech3.con
-cic:/matita/nat/bertrand/tech1.con
-cic:/matita/nat/bertrand/tech.con
-cic:/matita/nat/bertrand/sorted_lt.con
-cic:/matita/nat/bertrand/sorted_list_n_aux.con
-cic:/matita/nat/bertrand/sorted_gt.con
-cic:/matita/nat/bertrand/sieve_sound2.con
-cic:/matita/nat/bertrand/sieve_sound1.con
-cic:/matita/nat/bertrand/sieve_sorted.con
-cic:/matita/nat/bertrand/sieve_prime.con
-cic:/matita/nat/bertrand/sieve_aux.con
-cic:/matita/nat/bertrand/sieve.con
-cic:/matita/nat/bertrand/not_not_bertrand_to_bertrand1.con
-cic:/matita/nat/bertrand/not_not_bertrand_to_bertrand.con
-cic:/matita/nat/bertrand/not_bertrand_to_le_B.con
-cic:/matita/nat/bertrand/not_bertrand_to_le2.con
-cic:/matita/nat/bertrand/not_bertrand_to_le1.con
-cic:/matita/nat/bertrand/not_bertrand.con
-cic:/matita/nat/bertrand/min_prim.con
-cic:/matita/nat/bertrand/lt_to_div_O.con
-cic:/matita/nat/bertrand/lt_div_to_times.con
-cic:/matita/nat/bertrand/lt_div_S_div.con
-cic:/matita/nat/bertrand/lprim.con
-cic:/matita/nat/bertrand/list_of_primes_to_bertrand.con
-cic:/matita/nat/bertrand/list_of_primes.con
-cic:/matita/nat/bertrand/list_n_aux.con
-cic:/matita/nat/bertrand/list_n.con
-cic:/matita/nat/bertrand/list_divides.con
-cic:/matita/nat/bertrand/le_to_bertrand2.con
-cic:/matita/nat/bertrand/le_to_bertrand.con
-cic:/matita/nat/bertrand/le_times_div_m_m.con
-cic:/matita/nat/bertrand/le_list_n_r.con
-cic:/matita/nat/bertrand/le_list_n_aux_r.con
-cic:/matita/nat/bertrand/le_list_n_aux_k_k.con
-cic:/matita/nat/bertrand/le_list_n_aux.con
-cic:/matita/nat/bertrand/le_list_n.con
-cic:/matita/nat/bertrand/le_length_list_n.con
-cic:/matita/nat/bertrand/le_k.con
-cic:/matita/nat/bertrand/le_SSO_list_n.con
-cic:/matita/nat/bertrand/le_B_split2_exp.con
-cic:/matita/nat/bertrand/le_B_split1_teta.con
-cic:/matita/nat/bertrand/k1.con
-cic:/matita/nat/bertrand/k.con
-cic:/matita/nat/bertrand/in_list_sieve_to_prime.con
-cic:/matita/nat/bertrand/in_list_sieve_to_leq.con
-cic:/matita/nat/bertrand/in_list_SSO_list_n.con
-cic:/matita/nat/bertrand/exp_plus_SSO.con
-cic:/matita/nat/bertrand/eq_B_B1.con
-cic:/matita/nat/bertrand/eq_B1_times_B_split1_B_split2.con
-cic:/matita/nat/bertrand/divides_to_prime_divides.con
-cic:/matita/nat/bertrand/checker_sound.con
-cic:/matita/nat/bertrand/checker_cons.con
-cic:/matita/nat/bertrand/checker.con
-cic:/matita/nat/bertrand/check_list2.con
-cic:/matita/nat/bertrand/check_list1.con
-cic:/matita/nat/bertrand/check_list.con
-cic:/matita/nat/bertrand/bertrand_n.con
-cic:/matita/nat/bertrand/bertrand.con
-cic:/matita/nat/bertrand/B_split2.con
-cic:/matita/nat/bertrand/B_split1.con
-cic:/matita/nat/bertrand/B1.con
-cic:/matita/nat/binomial/lt_O_bc.con
-cic:/matita/nat/binomial/fact_minus.con
-cic:/matita/nat/binomial/exp_plus_sigma_p.con
-cic:/matita/nat/binomial/exp_Sn_SSO.con
-cic:/matita/nat/binomial/exp_S_sigma_p.con
-cic:/matita/nat/binomial/bc_n_n.con
-cic:/matita/nat/binomial/bc_n_O.con
-cic:/matita/nat/binomial/bc2.con
-cic:/matita/nat/binomial/bc1.con
-cic:/matita/nat/binomial/bc.con
-cic:/matita/nat/chebyshev/times_SSO_pred.con
-cic:/matita/nat/chebyshev/sigma_p_divides_b1.con
-cic:/matita/nat/chebyshev/sigma_p_divides_b.con
-cic:/matita/nat/chebyshev/prim.con
-cic:/matita/nat/chebyshev/pi_p_primeb_divides_b.con
-cic:/matita/nat/chebyshev/pi_p_primeb5.con
-cic:/matita/nat/chebyshev/pi_p_primeb4.con
-cic:/matita/nat/chebyshev/pi_p_primeb1.con
-cic:/matita/nat/chebyshev/pi_p_primeb.con
-cic:/matita/nat/chebyshev/not_prime_times_SSO.con
-cic:/matita/nat/chebyshev/monotonic_A.con
-cic:/matita/nat/chebyshev/lt_max_to_pi_p_primeb.con
-cic:/matita/nat/chebyshev/lt_SSSSO_to_le_B_exp.con
-cic:/matita/nat/chebyshev/lt_SSSSO_to_le_A_exp.con
-cic:/matita/nat/chebyshev/lt_SO_to_le_exp_B.con
-cic:/matita/nat/chebyshev/lt_SO_to_le_B_exp.con
-cic:/matita/nat/chebyshev/le_primr.con
-cic:/matita/nat/chebyshev/le_priml1.con
-cic:/matita/nat/chebyshev/le_priml.con
-cic:/matita/nat/chebyshev/le_prim_n3.con
-cic:/matita/nat/chebyshev/le_prim_n2.con
-cic:/matita/nat/chebyshev/le_prim_n1.con
-cic:/matita/nat/chebyshev/le_prim_n.con
-cic:/matita/nat/chebyshev/le_prim_log.con
-cic:/matita/nat/chebyshev/le_pred.con
-cic:/matita/nat/chebyshev/le_ord_log.con
-cic:/matita/nat/chebyshev/le_n_SSSSSSSSO_to_le_A_exp.con
-cic:/matita/nat/chebyshev/le_fact_A.con
-cic:/matita/nat/chebyshev/le_exp_primr.con
-cic:/matita/nat/chebyshev/le_exp_priml.con
-cic:/matita/nat/chebyshev/le_exp_prim4l.con
-cic:/matita/nat/chebyshev/le_exp_B.con
-cic:/matita/nat/chebyshev/le_S_times_SSO.con
-cic:/matita/nat/chebyshev/le_B_exp.con
-cic:/matita/nat/chebyshev/le_B_A4.con
-cic:/matita/nat/chebyshev/le_B_A.con
-cic:/matita/nat/chebyshev/le_Al1.con
-cic:/matita/nat/chebyshev/le_Al.con
-cic:/matita/nat/chebyshev/le_A_exp5.con
-cic:/matita/nat/chebyshev/le_A_exp4.con
-cic:/matita/nat/chebyshev/le_A_exp1.con
-cic:/matita/nat/chebyshev/le_A_exp.con
-cic:/matita/nat/chebyshev/le_A_BA1.con
-cic:/matita/nat/chebyshev/le_A_BA.con
-cic:/matita/nat/chebyshev/leA_r2.con
-cic:/matita/nat/chebyshev/leA_prim.con
-cic:/matita/nat/chebyshev/fact_pi_p3.con
-cic:/matita/nat/chebyshev/fact_pi_p2.con
-cic:/matita/nat/chebyshev/fact_pi_p.con
-cic:/matita/nat/chebyshev/exp_fact_SSO.con
-cic:/matita/nat/chebyshev/eq_sigma_pi_SO_n.con
-cic:/matita/nat/chebyshev/eq_sigma_p_div.con
-cic:/matita/nat/chebyshev/eq_prim_prim_pred.con
-cic:/matita/nat/chebyshev/eq_pi_p_primeb_divides_b.con
-cic:/matita/nat/chebyshev/eq_ord_sigma_p.con
-cic:/matita/nat/chebyshev/eq_fact_pi_p.con
-cic:/matita/nat/chebyshev/eq_fact_B.con
-cic:/matita/nat/chebyshev/eq_A_SSO_n.con
-cic:/matita/nat/chebyshev/eq_A_A'.con
-cic:/matita/nat/chebyshev/B_SSSSSSSSO.con
-cic:/matita/nat/chebyshev/B_SSSSSSSO.con
-cic:/matita/nat/chebyshev/B_SSSSSSO.con
-cic:/matita/nat/chebyshev/B_SSSSSO.con
-cic:/matita/nat/chebyshev/B_SSSSO.con
-cic:/matita/nat/chebyshev/B_SSSO.con
-cic:/matita/nat/chebyshev/B.con
-cic:/matita/nat/chebyshev/A_SSSSO.con
-cic:/matita/nat/chebyshev/A_SSSO.con
-cic:/matita/nat/chebyshev/A_SSO.con
-cic:/matita/nat/chebyshev/A_SO.con
-cic:/matita/nat/chebyshev/A.con
-cic:/matita/nat/chebyshev/A'.con
-cic:/matita/nat/chebyshev_teta/teta_pred.con
-cic:/matita/nat/chebyshev_teta/teta_pi_p_teta.con
-cic:/matita/nat/chebyshev_teta/teta.con
-cic:/matita/nat/chebyshev_teta/prime_to_divides_M.con
-cic:/matita/nat/chebyshev_teta/lt_O_to_le_teta_exp_teta.con
-cic:/matita/nat/chebyshev_teta/lt_O_teta.con
-cic:/matita/nat/chebyshev_teta/lt_M.con
-cic:/matita/nat/chebyshev_teta/le_teta_M_teta.con
-cic:/matita/nat/chebyshev_teta/le_teta.con
-cic:/matita/nat/chebyshev_teta/divides_pi_p_M1.con
-cic:/matita/nat/chebyshev_teta/divides_pi_p_M.con
-cic:/matita/nat/chebyshev_teta/divides_fact_to_le.con
-cic:/matita/nat/chebyshev_teta/divides_fact_to_divides.con
-cic:/matita/nat/chebyshev_teta/div_teta_teta.con
-cic:/matita/nat/chebyshev_teta/M.con
-cic:/matita/nat/chebyshev_thm/theta_pi.con
-cic:/matita/nat/chebyshev_thm/log_pi_p.con
-cic:/matita/nat/chebyshev_thm/le_log_C2_sigma_p.con
-cic:/matita/nat/chebyshev_thm/jj.con
-cic:/matita/nat/chebyshev_thm/daemon.con
-cic:/matita/nat/chebyshev_thm/asdasd.con
-cic:/matita/nat/chebyshev_thm/C2.con
-cic:/matita/nat/chebyshev_thm/C1.con
-cic:/matita/nat/chebyshev_thm/C.con
-cic:/matita/nat/chinese_reminder/mod_cr_pair.con
-cic:/matita/nat/chinese_reminder/cr_pair4.con
-cic:/matita/nat/chinese_reminder/cr_pair3.con
-cic:/matita/nat/chinese_reminder/cr_pair2.con
-cic:/matita/nat/chinese_reminder/cr_pair1.con
-cic:/matita/nat/chinese_reminder/cr_pair.con
-cic:/matita/nat/chinese_reminder/and_congruent_congruent_lt.con
-cic:/matita/nat/chinese_reminder/and_congruent_congruent.con
-cic:/matita/nat/compare/not_eq_to_eqb_false.con
-cic:/matita/nat/compare/nat_compare_to_Prop.con
-cic:/matita/nat/compare/nat_compare_pred_pred.con
-cic:/matita/nat/compare/nat_compare_n_n.con
-cic:/matita/nat/compare/nat_compare_n_m_m_n.con
-cic:/matita/nat/compare/nat_compare_elim.con
-cic:/matita/nat/compare/nat_compare_S_S.con
-cic:/matita/nat/compare/nat_compare.con
-cic:/matita/nat/compare/ltb_to_Prop.con
-cic:/matita/nat/compare/ltb_elim.con
-cic:/matita/nat/compare/ltb.con
-cic:/matita/nat/compare/lt_to_leb_false.con
-cic:/matita/nat/compare/leb_true_to_le.con
-cic:/matita/nat/compare/leb_to_Prop.con
-cic:/matita/nat/compare/leb_false_to_not_le.con
-cic:/matita/nat/compare/leb_elim.con
-cic:/matita/nat/compare/leb.con
-cic:/matita/nat/compare/le_to_leb_true.con
-cic:/matita/nat/compare/eqb_true_to_eq.con
-cic:/matita/nat/compare/eqb_to_Prop.con
-cic:/matita/nat/compare/eqb_n_n.con
-cic:/matita/nat/compare/eqb_false_to_not_eq.con
-cic:/matita/nat/compare/eqb_elim.con
-cic:/matita/nat/compare/eqb.con
-cic:/matita/nat/compare/eq_to_eqb_true.con
-cic:/matita/nat/congruence/transitive_congruent.con
-cic:/matita/nat/congruence/mod_times_mod.con
-cic:/matita/nat/congruence/mod_times.con
-cic:/matita/nat/congruence/mod_mod.con
-cic:/matita/nat/congruence/le_to_mod.con
-cic:/matita/nat/congruence/eq_times_plus_to_congruent.con
-cic:/matita/nat/congruence/divides_to_congruent.con
-cic:/matita/nat/congruence/congruent_to_divides.con
-cic:/matita/nat/congruence/congruent_times.con
-cic:/matita/nat/congruence/congruent_pi.con
-cic:/matita/nat/congruence/congruent_n_n.con
-cic:/matita/nat/congruence/congruent_n_mod_times.con
-cic:/matita/nat/congruence/congruent_n_mod_n.con
-cic:/matita/nat/congruence/congruent.con
-cic:/matita/nat/congruence/S_mod.con
-cic:/matita/nat/count/sigma_times.con
-cic:/matita/nat/count/sigma_plus1.con
-cic:/matita/nat/count/sigma_plus.con
-cic:/matita/nat/count/sigma_f_g.con
-cic:/matita/nat/count/eq_sigma_sigma1.con
-cic:/matita/nat/count/eq_sigma_sigma.con
-cic:/matita/nat/count/count_times.con
-cic:/matita/nat/count/count.con
-cic:/matita/nat/count/bool_to_nat_andb.con
-cic:/matita/nat/count/bool_to_nat.con
-cic:/matita/nat/div_and_mod/or_div_mod.con
-cic:/matita/nat/div_and_mod/n_divides_aux.con
-cic:/matita/nat/div_and_mod/n_divides.con
-cic:/matita/nat/div_and_mod/mod_plus_times.con
-cic:/matita/nat/div_and_mod/mod_n_n.con
-cic:/matita/nat/div_and_mod/mod_aux.con
-cic:/matita/nat/div_and_mod/mod_SO.con
-cic:/matita/nat/div_and_mod/mod_S.con
-cic:/matita/nat/div_and_mod/mod_O_n.con
-cic:/matita/nat/div_and_mod/mod.con
-cic:/matita/nat/div_and_mod/lt_to_eq_mod.con
-cic:/matita/nat/div_and_mod/lt_mod_m_m.con
-cic:/matita/nat/div_and_mod/lt_O_to_injective_times_r.con
-cic:/matita/nat/div_and_mod/lt_O_to_injective_times_l.con
-cic:/matita/nat/div_and_mod/lt_O_to_div_times.con
-cic:/matita/nat/div_and_mod/le_mod_aux_m_m.con
-cic:/matita/nat/div_and_mod/injective_times_r.con
-cic:/matita/nat/div_and_mod/injective_times_l.con
-cic:/matita/nat/div_and_mod/inj_times_r1.con
-cic:/matita/nat/div_and_mod/inj_times_r.con
-cic:/matita/nat/div_and_mod/inj_times_l1.con
-cic:/matita/nat/div_and_mod/inj_times_l.con
-cic:/matita/nat/div_and_mod/eq_times_div_minus_mod.con
-cic:/matita/nat/div_and_mod/eq_div_O.con
-cic:/matita/nat/div_and_mod/div_times.con
-cic:/matita/nat/div_and_mod/div_plus_times.con
-cic:/matita/nat/div_and_mod/div_n_n.con
-cic:/matita/nat/div_and_mod/div_mod_spec_to_not_eq_O.con
-cic:/matita/nat/div_and_mod/div_mod_spec_to_eq2.con
-cic:/matita/nat/div_and_mod/div_mod_spec_to_eq.con
-cic:/matita/nat/div_and_mod/div_mod_spec_times.con
-cic:/matita/nat/div_and_mod/div_mod_spec_rect.con
-cic:/matita/nat/div_and_mod/div_mod_spec_rec.con
-cic:/matita/nat/div_and_mod/div_mod_spec_ind.con
-cic:/matita/nat/div_and_mod/div_mod_spec_div_mod.con
-cic:/matita/nat/div_and_mod/div_mod_spec.ind
-cic:/matita/nat/div_and_mod/div_mod.con
-cic:/matita/nat/div_and_mod/div_aux_mod_aux.con
-cic:/matita/nat/div_and_mod/div_aux.con
-cic:/matita/nat/div_and_mod/div_SO.con
-cic:/matita/nat/div_and_mod/div.con
-cic:/matita/nat/div_and_mod_diseq/monotonic_div.con
-cic:/matita/nat/div_and_mod_diseq/lt_times_to_lt_div.con
-cic:/matita/nat/div_and_mod_diseq/lt_times_to_lt.con
-cic:/matita/nat/div_and_mod_diseq/lt_m_nm.con
-cic:/matita/nat/div_and_mod_diseq/lt_div_S.con
-cic:/matita/nat/div_and_mod_diseq/lt_div.con
-cic:/matita/nat/div_and_mod_diseq/le_times_to_le_div2.con
-cic:/matita/nat/div_and_mod_diseq/le_times_to_le_div.con
-cic:/matita/nat/div_and_mod_diseq/le_times_div_div_times.con
-cic:/matita/nat/div_and_mod_diseq/le_plus_mod.con
-cic:/matita/nat/div_and_mod_diseq/le_plus_div.con
-cic:/matita/nat/div_and_mod_diseq/le_div_times_m.con
-cic:/matita/nat/div_and_mod_diseq/le_div_times_Sm.con
-cic:/matita/nat/div_and_mod_diseq/le_div_plus_S.con
-cic:/matita/nat/div_and_mod_diseq/le_div_S_S_div.con
-cic:/matita/nat/div_and_mod_diseq/le_div.con
-cic:/matita/nat/euler_theorem/totient_card_aux.con
-cic:/matita/nat/euler_theorem/totient_card.con
-cic:/matita/nat/euler_theorem/permut_p_mod.con
-cic:/matita/nat/euler_theorem/gcd_pi_p.con
-cic:/matita/nat/euler_theorem/congruent_map_iter_p_times.con
-cic:/matita/nat/euler_theorem/congruent_exp_totient_SO.con
-cic:/matita/nat/euler_theorem/card_Sn.con
-cic:/matita/nat/exp/times_exp.con
-cic:/matita/nat/exp/monotonic_exp1.con
-cic:/matita/nat/exp/lt_m_exp_nm.con
-cic:/matita/nat/exp/lt_exp_to_lt1.con
-cic:/matita/nat/exp/lt_exp_to_lt.con
-cic:/matita/nat/exp/lt_exp1.con
-cic:/matita/nat/exp/lt_exp.con
-cic:/matita/nat/exp/lt_O_exp.con
-cic:/matita/nat/exp/le_exp_to_le1.con
-cic:/matita/nat/exp/le_exp_to_le.con
-cic:/matita/nat/exp/le_exp.con
-cic:/matita/nat/exp/injective_exp_r.con
-cic:/matita/nat/exp/inj_exp_r.con
-cic:/matita/nat/exp/exp_to_eq_O.con
-cic:/matita/nat/exp/exp_plus_times.con
-cic:/matita/nat/exp/exp_n_SO.con
-cic:/matita/nat/exp/exp_n_O.con
-cic:/matita/nat/exp/exp_exp_times.con
-cic:/matita/nat/exp/exp_SSO.con
-cic:/matita/nat/exp/exp_SO_n.con
-cic:/matita/nat/exp/exp.con
-cic:/matita/nat/factorial/lt_n_fact_n.con
-cic:/matita/nat/factorial/le_n_fact_n.con
-cic:/matita/nat/factorial/le_SSO_fact.con
-cic:/matita/nat/factorial/le_SO_fact.con
-cic:/matita/nat/factorial/fact.con
-cic:/matita/nat/factorial2/lt_SSSSO_to_fact.con
-cic:/matita/nat/factorial2/lt_O_to_fact1.con
-cic:/matita/nat/factorial2/lt_O_fact.con
-cic:/matita/nat/factorial2/le_fact_10.con
-cic:/matita/nat/factorial2/factS.con
-cic:/matita/nat/factorial2/fact3.con
-cic:/matita/nat/factorial2/fact2.con
-cic:/matita/nat/factorial2/fact1.con
-cic:/matita/nat/factorial2/exp_S.con
-cic:/matita/nat/factorial2/ab_times_cd.con
-cic:/matita/nat/factorization/p_ord_to_lt_max_prime_factor1.con
-cic:/matita/nat/factorization/p_ord_to_lt_max_prime_factor.con
-cic:/matita/nat/factorization/not_eq_nf_last_nf_cons.con
-cic:/matita/nat/factorization/not_eq_nf_cons_O_nf_cons.con
-cic:/matita/nat/factorization/not_divides_defactorize_aux.con
-cic:/matita/nat/factorization/nat_fact_rect.con
-cic:/matita/nat/factorization/nat_fact_rec.con
-cic:/matita/nat/factorization/nat_fact_ind.con
-cic:/matita/nat/factorization/nat_fact_all_rect.con
-cic:/matita/nat/factorization/nat_fact_all_rec.con
-cic:/matita/nat/factorization/nat_fact_all_ind.con
-cic:/matita/nat/factorization/nat_fact_all.ind
-cic:/matita/nat/factorization/nat_fact.ind
-cic:/matita/nat/factorization/max_prime_factor_to_not_p_ord_O.con
-cic:/matita/nat/factorization/max_prime_factor.con
-cic:/matita/nat/factorization/max_p_exponent.con
-cic:/matita/nat/factorization/max_p.con
-cic:/matita/nat/factorization/lt_max_prime_factor_to_not_divides.con
-cic:/matita/nat/factorization/lt_SO_max_prime.con
-cic:/matita/nat/factorization/lt_SO_defactorize_aux.con
-cic:/matita/nat/factorization/lt_O_defactorize_aux.con
-cic:/matita/nat/factorization/injective_defactorize_aux.con
-cic:/matita/nat/factorization/injective_defactorize.con
-cic:/matita/nat/factorization/factorize_defactorize.con
-cic:/matita/nat/factorization/factorize_aux.con
-cic:/matita/nat/factorization/factorize.con
-cic:/matita/nat/factorization/eq_p_max.con
-cic:/matita/nat/factorization/eq_defactorize_aux_to_eq.con
-cic:/matita/nat/factorization/divides_to_max_prime_factor1.con
-cic:/matita/nat/factorization/divides_to_max_prime_factor.con
-cic:/matita/nat/factorization/divides_max_prime_factor_n.con
-cic:/matita/nat/factorization/divides_max_p_defactorize.con
-cic:/matita/nat/factorization/defactorize_factorize.con
-cic:/matita/nat/factorization/defactorize_aux_factorize_aux.con
-cic:/matita/nat/factorization/defactorize_aux.con
-cic:/matita/nat/factorization/defactorize.con
-cic:/matita/nat/fermat_little_theorem/prime_to_not_divides_fact.con
-cic:/matita/nat/fermat_little_theorem/permut_mod.con
-cic:/matita/nat/fermat_little_theorem/permut_S_mod.con
-cic:/matita/nat/fermat_little_theorem/congruent_exp_pred_SO.con
-cic:/matita/nat/gcd/symmetric_gcd.con
-cic:/matita/nat/gcd/sym_gcd.con
-cic:/matita/nat/gcd/prime_to_gcd_SO.con
-cic:/matita/nat/gcd/lt_O_gcd.con
-cic:/matita/nat/gcd/le_gcd_times.con
-cic:/matita/nat/gcd/gcd_times_SO_to_gcd_SO.con
-cic:/matita/nat/gcd/gcd_n_times_nm.con
-cic:/matita/nat/gcd/gcd_n_n.con
-cic:/matita/nat/gcd/gcd_mod.con
-cic:/matita/nat/gcd/gcd_aux.con
-cic:/matita/nat/gcd/gcd_SO_to_lt_n.con
-cic:/matita/nat/gcd/gcd_SO_to_lt_O.con
-cic:/matita/nat/gcd/gcd_SO_to_divides_times_to_divides.con
-cic:/matita/nat/gcd/gcd_SO_n.con
-cic:/matita/nat/gcd/gcd_O_to_eq_O.con
-cic:/matita/nat/gcd/gcd_O_n.con
-cic:/matita/nat/gcd/gcd.con
-cic:/matita/nat/gcd/eq_minus_gcd_aux.con
-cic:/matita/nat/gcd/eq_minus_gcd.con
-cic:/matita/nat/gcd/eq_gcd_times_SO.con
-cic:/matita/nat/gcd/eq_gcd_SO_to_not_divides.con
-cic:/matita/nat/gcd/divides_to_divides_times.con
-cic:/matita/nat/gcd/divides_times_to_divides.con
-cic:/matita/nat/gcd/divides_times_gcd_aux.con
-cic:/matita/nat/gcd/divides_mod_to_divides.con
-cic:/matita/nat/gcd/divides_mod_gcd.con
-cic:/matita/nat/gcd/divides_mod.con
-cic:/matita/nat/gcd/divides_gcd_nm.con
-cic:/matita/nat/gcd/divides_gcd_n.con
-cic:/matita/nat/gcd/divides_gcd_mod.con
-cic:/matita/nat/gcd/divides_gcd_m.con
-cic:/matita/nat/gcd/divides_gcd_aux_mn.con
-cic:/matita/nat/gcd/divides_gcd_aux.con
-cic:/matita/nat/gcd/divides_exp_to_eq.con
-cic:/matita/nat/gcd/divides_exp_to_divides.con
-cic:/matita/nat/gcd/divides_d_times_gcd.con
-cic:/matita/nat/gcd/divides_d_gcd.con
-cic:/matita/nat/gcd_properties1/gcd_plus_times_gcd.con
-cic:/matita/nat/gcd_properties1/gcd_SO_to_eq_gcd_times_times_gcd_gcd.con
-cic:/matita/nat/gcd_properties1/gcd_SO_to_divides_to_divides_to_divides_times.con
-cic:/matita/nat/gcd_properties1/gcd1.con
-cic:/matita/nat/gcd_properties1/eq_gcd_times_times_times_gcd.con
-cic:/matita/nat/gcd_properties1/eq_gcd_gcd_minus.con
-cic:/matita/nat/gcd_properties1/eq_gcd_div_div_div_gcd.con
-cic:/matita/nat/gcd_properties1/divides_times_to_divides_div_gcd.con
-cic:/matita/nat/gcd_properties1/associative_nat_gcd.con
-cic:/matita/nat/generic_iter_p/true_to_iter_p_gen_Sn.con
-cic:/matita/nat/generic_iter_p/p_ord_times.con
-cic:/matita/nat/generic_iter_p/or_false_eq_baseA_to_eq_iter_p_gen.con
-cic:/matita/nat/generic_iter_p/mod_p_ord_times.con
-cic:/matita/nat/generic_iter_p/lt_times_to_lt_O.con
-cic:/matita/nat/generic_iter_p/iter_p_gen_plusA.con
-cic:/matita/nat/generic_iter_p/iter_p_gen_knm.con
-cic:/matita/nat/generic_iter_p/iter_p_gen_iter_p_gen.con
-cic:/matita/nat/generic_iter_p/iter_p_gen_gi.con
-cic:/matita/nat/generic_iter_p/iter_p_gen_false.con
-cic:/matita/nat/generic_iter_p/iter_p_gen_divides.con
-cic:/matita/nat/generic_iter_p/iter_p_gen_2_eq.con
-cic:/matita/nat/generic_iter_p/iter_p_gen2.con
-cic:/matita/nat/generic_iter_p/iter_p_gen2'.con
-cic:/matita/nat/generic_iter_p/iter_p_gen.con
-cic:/matita/nat/generic_iter_p/false_to_iter_p_gen_Sn.con
-cic:/matita/nat/generic_iter_p/false_to_eq_iter_p_gen.con
-cic:/matita/nat/generic_iter_p/eq_p_ord_times.con
-cic:/matita/nat/generic_iter_p/eq_iter_p_gen_pred.con
-cic:/matita/nat/generic_iter_p/eq_iter_p_gen_gh.con
-cic:/matita/nat/generic_iter_p/eq_iter_p_gen1.con
-cic:/matita/nat/generic_iter_p/eq_iter_p_gen.con
-cic:/matita/nat/generic_iter_p/div_p_ord_times.con
-cic:/matita/nat/generic_iter_p/distributive_times_plus_iter_p_gen.con
-cic:/matita/nat/iteration2/true_to_sigma_p_Sn.con
-cic:/matita/nat/iteration2/symmetricIntPlus.con
-cic:/matita/nat/iteration2/sigma_p_true.con
-cic:/matita/nat/iteration2/sigma_p_times.con
-cic:/matita/nat/iteration2/sigma_p_sigma_p.con
-cic:/matita/nat/iteration2/sigma_p_plus_1.con
-cic:/matita/nat/iteration2/sigma_p_plus.con
-cic:/matita/nat/iteration2/sigma_p_knm.con
-cic:/matita/nat/iteration2/sigma_p_gi.con
-cic:/matita/nat/iteration2/sigma_p_false.con
-cic:/matita/nat/iteration2/sigma_p_divides.con
-cic:/matita/nat/iteration2/sigma_p2_eq.con
-cic:/matita/nat/iteration2/sigma_p2.con
-cic:/matita/nat/iteration2/sigma_p2'.con
-cic:/matita/nat/iteration2/sigma_p.con
-cic:/matita/nat/iteration2/sigma_P_SO_to_sigma_p_true.con
-cic:/matita/nat/iteration2/or_false_to_eq_sigma_p.con
-cic:/matita/nat/iteration2/lt_sigma_p.con
-cic:/matita/nat/iteration2/le_sigma_p1.con
-cic:/matita/nat/iteration2/le_sigma_p.con
-cic:/matita/nat/iteration2/false_to_sigma_p_Sn.con
-cic:/matita/nat/iteration2/false_to_eq_sigma_p.con
-cic:/matita/nat/iteration2/eq_sigma_p_sigma_p_times2.con
-cic:/matita/nat/iteration2/eq_sigma_p_sigma_p_times1.con
-cic:/matita/nat/iteration2/eq_sigma_p_pred.con
-cic:/matita/nat/iteration2/eq_sigma_p_gh.con
-cic:/matita/nat/iteration2/eq_sigma_p1.con
-cic:/matita/nat/iteration2/eq_sigma_p.con
-cic:/matita/nat/iteration2/eq_map_iter_i_sigma_p_alwaysTrue.con
-cic:/matita/nat/iteration2/distributive_times_plus_sigma_p.con
-cic:/matita/nat/iteration2/bool_to_nat_to_eq_sigma_p.con
-cic:/matita/nat/le_arith/monotonic_le_times_r.con
-cic:/matita/nat/le_arith/monotonic_le_times_l.con
-cic:/matita/nat/le_arith/monotonic_le_plus_r.con
-cic:/matita/nat/le_arith/monotonic_le_plus_l.con
-cic:/matita/nat/le_arith/le_times_to_le.con
-cic:/matita/nat/le_arith/le_times_r.con
-cic:/matita/nat/le_arith/le_times_n.con
-cic:/matita/nat/le_arith/le_times_l.con
-cic:/matita/nat/le_arith/le_times.con
-cic:/matita/nat/le_arith/le_plus_to_le.con
-cic:/matita/nat/le_arith/le_plus_r.con
-cic:/matita/nat/le_arith/le_plus_n_r.con
-cic:/matita/nat/le_arith/le_plus_n.con
-cic:/matita/nat/le_arith/le_plus_l.con
-cic:/matita/nat/le_arith/le_plus.con
-cic:/matita/nat/le_arith/le_S_times_SSO.con
-cic:/matita/nat/le_arith/eq_plus_to_le.con
-cic:/matita/nat/le_arith/O_lt_const_to_le_times_const.con
-cic:/matita/nat/log/lt_to_log_O.con
-cic:/matita/nat/log/lt_log_n_n.con
-cic:/matita/nat/log/lt_exp_log.con
-cic:/matita/nat/log/lt_O_log.con
-cic:/matita/nat/log/log_times_l.con
-cic:/matita/nat/log/log_times1.con
-cic:/matita/nat/log/log_times.con
-cic:/matita/nat/log/log_n_n.con
-cic:/matita/nat/log/log_i_SSOn.con
-cic:/matita/nat/log/log_exp2.con
-cic:/matita/nat/log/log_exp1.con
-cic:/matita/nat/log/log_exp.con
-cic:/matita/nat/log/log_div.con
-cic:/matita/nat/log/log_SO.con
-cic:/matita/nat/log/log.con
-cic:/matita/nat/log/le_log_plus.con
-cic:/matita/nat/log/le_log_n_n.con
-cic:/matita/nat/log/le_log.con
-cic:/matita/nat/log/le_exp_log.con
-cic:/matita/nat/log/exp_n_O.con
-cic:/matita/nat/log/eq_log_exp.con
-cic:/matita/nat/lt_arith/times_mod.con
-cic:/matita/nat/lt_arith/nat_compare_times_l.con
-cic:/matita/nat/lt_arith/monotonic_to_injective.con
-cic:/matita/nat/lt_arith/monotonic_lt_times_variant.con
-cic:/matita/nat/lt_arith/monotonic_lt_times_r.con
-cic:/matita/nat/lt_arith/monotonic_lt_times_l.con
-cic:/matita/nat/lt_arith/monotonic_lt_plus_r.con
-cic:/matita/nat/lt_arith/monotonic_lt_plus_l.con
-cic:/matita/nat/lt_arith/lt_to_lt_to_eq_div_div_times_times.con
-cic:/matita/nat/lt_arith/lt_to_le_to_lt_times.con
-cic:/matita/nat/lt_arith/lt_to_le_times_to_lt_S_to_div.con
-cic:/matita/nat/lt_arith/lt_to_div_to_and_le_times_lt_S.con
-cic:/matita/nat/lt_arith/lt_times_to_lt_r.con
-cic:/matita/nat/lt_arith/lt_times_to_lt_l.con
-cic:/matita/nat/lt_arith/lt_times_to_lt_O.con
-cic:/matita/nat/lt_arith/lt_times_r1.con
-cic:/matita/nat/lt_arith/lt_times_r.con
-cic:/matita/nat/lt_arith/lt_times_plus_times.con
-cic:/matita/nat/lt_arith/lt_times_n_to_lt_r.con
-cic:/matita/nat/lt_arith/lt_times_n_to_lt.con
-cic:/matita/nat/lt_arith/lt_times_l1.con
-cic:/matita/nat/lt_arith/lt_times_l.con
-cic:/matita/nat/lt_arith/lt_times_eq_O.con
-cic:/matita/nat/lt_arith/lt_times.con
-cic:/matita/nat/lt_arith/lt_plus_to_lt_r.con
-cic:/matita/nat/lt_arith/lt_plus_to_lt_l.con
-cic:/matita/nat/lt_arith/lt_plus_r.con
-cic:/matita/nat/lt_arith/lt_plus_l.con
-cic:/matita/nat/lt_arith/lt_plus.con
-cic:/matita/nat/lt_arith/lt_div_n_m_n.con
-cic:/matita/nat/lt_arith/lt_O_times_S_S.con
-cic:/matita/nat/lt_arith/le_to_lt_to_plus_lt.con
-cic:/matita/nat/lt_arith/increasing_to_injective.con
-cic:/matita/nat/lt_arith/eq_mod_O_to_lt_O_div.con
-cic:/matita/nat/lt_arith/eq_div_div_div_times.con
-cic:/matita/nat/lt_arith/eq_div_div_div_div.con
-cic:/matita/nat/lt_arith/SSO_mod.con
-cic:/matita/nat/lt_arith/O_lt_times_to_O_lt.con
-cic:/matita/nat/map_iter_p/pi_p_S.con
-cic:/matita/nat/map_iter_p/pi_p.con
-cic:/matita/nat/map_iter_p/permut_p_transpose.con
-cic:/matita/nat/map_iter_p/permut_p_compose.con
-cic:/matita/nat/map_iter_p/permut_p_S_to_permut_p.con
-cic:/matita/nat/map_iter_p/permut_p_O.con
-cic:/matita/nat/map_iter_p/permut_p.con
-cic:/matita/nat/map_iter_p/map_iter_p_S_true.con
-cic:/matita/nat/map_iter_p/map_iter_p_S_false.con
-cic:/matita/nat/map_iter_p/map_iter_p_O.con
-cic:/matita/nat/map_iter_p/map_iter_p.con
-cic:/matita/nat/map_iter_p/lt_O_pi_p.con
-cic:/matita/nat/map_iter_p/extentional_eq_n_to_permut_p.con
-cic:/matita/nat/map_iter_p/extentional_eq_n.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose3.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose2.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose1.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p_permut.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p_k.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p_a.con
-cic:/matita/nat/map_iter_p/eq_map_iter_p.con
-cic:/matita/nat/map_iter_p/decidable_n2.con
-cic:/matita/nat/map_iter_p/decidable_n1.con
-cic:/matita/nat/map_iter_p/decidable_n.con
-cic:/matita/nat/map_iter_p/count_card1.con
-cic:/matita/nat/map_iter_p/count_card.con
-cic:/matita/nat/map_iter_p/card.con
-cic:/matita/nat/map_iter_p/a_times_pi_p.con
-cic:/matita/nat/minimization/min_aux_S.con
-cic:/matita/nat/minimization/min_aux_O_f.con
-cic:/matita/nat/minimization/min_aux.con
-cic:/matita/nat/minimization/min_O_f.con
-cic:/matita/nat/minimization/min.con
-cic:/matita/nat/minimization/max_spec_to_max.con
-cic:/matita/nat/minimization/max_spec.con
-cic:/matita/nat/minimization/max_f_g.con
-cic:/matita/nat/minimization/max_S_max.con
-cic:/matita/nat/minimization/max_O_f.con
-cic:/matita/nat/minimization/max_O.con
-cic:/matita/nat/minimization/max.con
-cic:/matita/nat/minimization/lt_min_aux_to_false.con
-cic:/matita/nat/minimization/lt_max_to_false.con
-cic:/matita/nat/minimization/le_to_le_max.con
-cic:/matita/nat/minimization/le_min_aux_r.con
-cic:/matita/nat/minimization/le_min_aux.con
-cic:/matita/nat/minimization/le_max_n.con
-cic:/matita/nat/minimization/le_max_f_max_g.con
-cic:/matita/nat/minimization/false_to_lt_max.con
-cic:/matita/nat/minimization/f_min_aux_true.con
-cic:/matita/nat/minimization/f_max_true.con
-cic:/matita/nat/minimization/f_m_to_le_max.con
-cic:/matita/nat/minimization/f_false_to_le_max.con
-cic:/matita/nat/minimization/exists_max_forall_false.con
-cic:/matita/nat/minimization/exists_forall_le.con
-cic:/matita/nat/minus/plus_to_minus.con
-cic:/matita/nat/minus/plus_minus_m_m.con
-cic:/matita/nat/minus/plus_minus.con
-cic:/matita/nat/minus/monotonic_le_minus_r.con
-cic:/matita/nat/minus/minus_to_plus.con
-cic:/matita/nat/minus/minus_pred_pred.con
-cic:/matita/nat/minus/minus_plus_m_m.con
-cic:/matita/nat/minus/minus_n_n.con
-cic:/matita/nat/minus/minus_n_O.con
-cic:/matita/nat/minus/minus_m_minus_mn.con
-cic:/matita/nat/minus/minus_le_S_minus_S.con
-cic:/matita/nat/minus/minus_le_O_to_le.con
-cic:/matita/nat/minus/minus_Sn_n.con
-cic:/matita/nat/minus/minus_Sn_m.con
-cic:/matita/nat/minus/minus_S_S.con
-cic:/matita/nat/minus/minus.con
-cic:/matita/nat/minus/lt_to_lt_O_minus.con
-cic:/matita/nat/minus/lt_plus_to_lt_minus.con
-cic:/matita/nat/minus/lt_minus_to_plus.con
-cic:/matita/nat/minus/lt_minus_to_lt_plus.con
-cic:/matita/nat/minus/lt_minus_r.con
-cic:/matita/nat/minus/lt_minus_m.con
-cic:/matita/nat/minus/lt_minus_l.con
-cic:/matita/nat/minus/lt_minus_S_n_to_le_minus_n.con
-cic:/matita/nat/minus/lt_O_minus_to_lt.con
-cic:/matita/nat/minus/le_plus_to_minus_r.con
-cic:/matita/nat/minus/le_plus_to_minus.con
-cic:/matita/nat/minus/le_minus_to_plus.con
-cic:/matita/nat/minus/le_minus_m.con
-cic:/matita/nat/minus/le_SO_minus.con
-cic:/matita/nat/minus/eq_plus_minus_minus_minus.con
-cic:/matita/nat/minus/eq_minus_plus_plus_minus.con
-cic:/matita/nat/minus/eq_minus_n_m_O.con
-cic:/matita/nat/minus/eq_minus_minus_minus_plus.con
-cic:/matita/nat/minus/eq_minus_S_pred.con
-cic:/matita/nat/minus/distributive_times_minus.con
-cic:/matita/nat/minus/distr_times_minus.con
-cic:/matita/nat/nat/pred_Sn.con
-cic:/matita/nat/nat/pred.con
-cic:/matita/nat/nat/not_zero.con
-cic:/matita/nat/nat/not_eq_n_Sn.con
-cic:/matita/nat/nat/not_eq_S.con
-cic:/matita/nat/nat/not_eq_O_S.con
-cic:/matita/nat/nat/nat_rect.con
-cic:/matita/nat/nat/nat_rec.con
-cic:/matita/nat/nat/nat_ind.con
-cic:/matita/nat/nat/nat_elim2.con
-cic:/matita/nat/nat/nat_case1.con
-cic:/matita/nat/nat/nat_case.con
-cic:/matita/nat/nat/nat.ind
-cic:/matita/nat/nat/injective_S.con
-cic:/matita/nat/nat/inj_S.con
-cic:/matita/nat/nat/decidable_eq_nat.con
-cic:/matita/nat/neper/sigma_p_log_div2.con
-cic:/matita/nat/neper/sigma_p_log_div1.con
-cic:/matita/nat/neper/sigma_p_log_div.con
-cic:/matita/nat/neper/sigma_p_div_exp.con
-cic:/matita/nat/neper/neper_sigma_p3.con
-cic:/matita/nat/neper/neper_sigma_p2.con
-cic:/matita/nat/neper/neper_sigma_p1.con
-cic:/matita/nat/neper/neper_monotonic.con
-cic:/matita/nat/neper/lt_exp_sigma_p_exp.con
-cic:/matita/nat/neper/lt_exp_Sn_n_SSSO.con
-cic:/matita/nat/neper/lt_exp_Sn_m_SSSO.con
-cic:/matita/nat/neper/lt_SO_to_lt_exp_Sn_n_SSSO.con
-cic:/matita/nat/neper/le_sigma_p_div_log_div_pred_log.con
-cic:/matita/nat/neper/le_log_exp_fact_sigma_p.con
-cic:/matita/nat/neper/le_log_exp_Sn_log_exp_n.con
-cic:/matita/nat/neper/le_log_div_sigma_p.con
-cic:/matita/nat/neper/le_fact_exp1.con
-cic:/matita/nat/neper/le_fact_exp.con
-cic:/matita/nat/neper/le_exp_sigma_p_exp.con
-cic:/matita/nat/neper/le_exp_div.con
-cic:/matita/nat/neper/le_exp_SSO_fact.con
-cic:/matita/nat/neper/le_SSO_neper.con
-cic:/matita/nat/neper/le_SSO_exp_neper.con
-cic:/matita/nat/neper/eq_fact_pi_p.con
-cic:/matita/nat/neper/eq_exp_pi_p.con
-cic:/matita/nat/neper/divides_times_to_eq.con
-cic:/matita/nat/neper/divides_times_to_divides_div.con
-cic:/matita/nat/neper/divides_sigma_p_to_eq.con
-cic:/matita/nat/neper/divides_pi_p_to_eq.con
-cic:/matita/nat/neper/divides_pi_p.con
-cic:/matita/nat/neper/divides_fact_fact.con
-cic:/matita/nat/nth_prime/smallest_factor_fact.con
-cic:/matita/nat/nth_prime/prime_to_nth_prime.con
-cic:/matita/nat/nth_prime/prime_nth_prime.con
-cic:/matita/nat/nth_prime/nth_prime.con
-cic:/matita/nat/nth_prime/lt_nth_prime_to_not_prime.con
-cic:/matita/nat/nth_prime/lt_nth_prime_n_nth_prime_Sn.con
-cic:/matita/nat/nth_prime/lt_n_nth_prime_n.con
-cic:/matita/nat/nth_prime/lt_SO_nth_prime_n.con
-cic:/matita/nat/nth_prime/lt_O_nth_prime_n.con
-cic:/matita/nat/nth_prime/injective_nth_prime.con
-cic:/matita/nat/nth_prime/increasing_nth_prime.con
-cic:/matita/nat/nth_prime/ex_prime.con
-cic:/matita/nat/nth_prime/ex_m_le_n_nth_prime_m.con
-cic:/matita/nat/o/lt_times_SSO_n_exp_SSO_n.con
-cic:/matita/nat/o/lt_exp_n_SSO_exp_SSO_n.con
-cic:/matita/nat/o/le_times_n_exp.con
-cic:/matita/nat/o/le_times_exp_n_SSO_exp_SSO_n.con
-cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con
-cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n1.con
-cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n.con
-cic:/matita/nat/ord/p_ord_to_not_eq_O.con
-cic:/matita/nat/ord/p_ord_to_exp1.con
-cic:/matita/nat/ord/p_ord_times.con
-cic:/matita/nat/ord/p_ord_p.con
-cic:/matita/nat/ord/p_ord_inv.con
-cic:/matita/nat/ord/p_ord_exp1.con
-cic:/matita/nat/ord/p_ord_exp.con
-cic:/matita/nat/ord/p_ord_aux_to_not_mod_O.con
-cic:/matita/nat/ord/p_ord_aux_to_exp.con
-cic:/matita/nat/ord/p_ord_aux_to_Prop1.con
-cic:/matita/nat/ord/p_ord_aux_to_Prop.con
-cic:/matita/nat/ord/p_ord_aux.con
-cic:/matita/nat/ord/p_ord_O_to_not_divides.con
-cic:/matita/nat/ord/p_ord.con
-cic:/matita/nat/ord/ord_times.con
-cic:/matita/nat/ord/ord_rem.con
-cic:/matita/nat/ord/ord_ord_rem.con
-cic:/matita/nat/ord/ord_exp.con
-cic:/matita/nat/ord/ord_O_to_not_divides.con
-cic:/matita/nat/ord/ord.con
-cic:/matita/nat/ord/not_ord_O_to_divides.con
-cic:/matita/nat/ord/not_divides_to_p_ord_O.con
-cic:/matita/nat/ord/not_divides_to_ord_O.con
-cic:/matita/nat/ord/not_divides_ord_rem.con
-cic:/matita/nat/ord/mod_p_ord_inv.con
-cic:/matita/nat/ord/lt_ord_rem.con
-cic:/matita/nat/ord/lt_O_ord_rem.con
-cic:/matita/nat/ord/fst_p_ord_times.con
-cic:/matita/nat/ord/exp_ord.con
-cic:/matita/nat/ord/eq_p_ord_inv.con
-cic:/matita/nat/ord/divides_to_p_ord.con
-cic:/matita/nat/ord/divides_to_ord.con
-cic:/matita/nat/ord/divides_to_not_ord_O.con
-cic:/matita/nat/ord/divides_to_le_ord.con
-cic:/matita/nat/ord/divides_to_divides_ord_rem.con
-cic:/matita/nat/ord/divides_ord_rem.con
-cic:/matita/nat/ord/div_p_ord_inv.con
-cic:/matita/nat/orders/transitive_lt.con
-cic:/matita/nat/orders/transitive_le.con
-cic:/matita/nat/orders/trans_lt.con
-cic:/matita/nat/orders/trans_le.con
-cic:/matita/nat/orders/not_lt_to_le.con
-cic:/matita/nat/orders/not_le_to_lt.con
-cic:/matita/nat/orders/not_le_Sn_n.con
-cic:/matita/nat/orders/not_le_Sn_O.con
-cic:/matita/nat/orders/not_eq_to_le_to_lt.con
-cic:/matita/nat/orders/nat_elim1.con
-cic:/matita/nat/orders/ltn_to_ltO.con
-cic:/matita/nat/orders/lt_to_not_le.con
-cic:/matita/nat/orders/lt_to_not_eq.con
-cic:/matita/nat/orders/lt_to_lt_S_S.con
-cic:/matita/nat/orders/lt_to_le_to_lt.con
-cic:/matita/nat/orders/lt_to_le.con
-cic:/matita/nat/orders/lt_pred.con
-cic:/matita/nat/orders/lt_n_m_to_not_lt_m_Sn.con
-cic:/matita/nat/orders/lt_S_to_lt.con
-cic:/matita/nat/orders/lt_S_to_le.con
-cic:/matita/nat/orders/lt_S_S_to_lt.con
-cic:/matita/nat/orders/lt_SO_n_to_lt_O_pred_n.con
-cic:/matita/nat/orders/lt_O_n_elim.con
-cic:/matita/nat/orders/lt_O_S.con
-cic:/matita/nat/orders/lt.con
-cic:/matita/nat/orders/le_to_or_lt_eq.con
-cic:/matita/nat/orders/le_to_not_lt.con
-cic:/matita/nat/orders/le_to_lt_to_lt.con
-cic:/matita/nat/orders/le_to_le_to_eq.con
-cic:/matita/nat/orders/le_to_le_pred.con
-cic:/matita/nat/orders/le_pred_to_le.con
-cic:/matita/nat/orders/le_pred_n.con
-cic:/matita/nat/orders/le_n_m_to_lt_m_Sn_to_eq_n_m.con
-cic:/matita/nat/orders/le_n_fn.con
-cic:/matita/nat/orders/le_n_Sn.con
-cic:/matita/nat/orders/le_n_Sm_elim.con
-cic:/matita/nat/orders/le_n_O_to_eq.con
-cic:/matita/nat/orders/le_n_O_elim.con
-cic:/matita/nat/orders/le_inv.con
-cic:/matita/nat/orders/le_ind.con
-cic:/matita/nat/orders/le_S_S_to_le.con
-cic:/matita/nat/orders/le_S_S.con
-cic:/matita/nat/orders/le_O_n.con
-cic:/matita/nat/orders/leS_to_not_zero.con
-cic:/matita/nat/orders/le.ind
-cic:/matita/nat/orders/increasing_to_monotonic.con
-cic:/matita/nat/orders/increasing_to_le2.con
-cic:/matita/nat/orders/increasing_to_le.con
-cic:/matita/nat/orders/increasing.con
-cic:/matita/nat/orders/gt.con
-cic:/matita/nat/orders/ge.con
-cic:/matita/nat/orders/eq_to_not_lt.con
-cic:/matita/nat/orders/decidable_lt.con
-cic:/matita/nat/orders/decidable_le.con
-cic:/matita/nat/orders/antisymmetric_le.con
-cic:/matita/nat/orders/antisym_le.con
-cic:/matita/nat/orders/S_pred.con
-cic:/matita/nat/orders/Not_lt_n_n.con
-cic:/matita/nat/permutation/transpose_transpose.con
-cic:/matita/nat/permutation/transpose_i_j_j_i.con
-cic:/matita/nat/permutation/transpose_i_j_j.con
-cic:/matita/nat/permutation/transpose_i_j_i.con
-cic:/matita/nat/permutation/transpose_i_i.con
-cic:/matita/nat/permutation/transpose.con
-cic:/matita/nat/permutation/permut_transpose_r.con
-cic:/matita/nat/permutation/permut_transpose_l.con
-cic:/matita/nat/permutation/permut_transpose.con
-cic:/matita/nat/permutation/permut_to_eq_map_iter_i.con
-cic:/matita/nat/permutation/permut_to_bijn.con
-cic:/matita/nat/permutation/permut_n_to_le.con
-cic:/matita/nat/permutation/permut_n_to_eq_n.con
-cic:/matita/nat/permutation/permut_invert_permut.con
-cic:/matita/nat/permutation/permut_fg.con
-cic:/matita/nat/permutation/permut_S_to_permut_transpose.con
-cic:/matita/nat/permutation/permut_S_to_permut.con
-cic:/matita/nat/permutation/permut_O_to_eq_O.con
-cic:/matita/nat/permutation/permut.con
-cic:/matita/nat/permutation/map_iter_i.con
-cic:/matita/nat/permutation/invert_permut_f.con
-cic:/matita/nat/permutation/invert_permut.con
-cic:/matita/nat/permutation/injn_Sn_n.con
-cic:/matita/nat/permutation/injn.con
-cic:/matita/nat/permutation/injective_transpose.con
-cic:/matita/nat/permutation/injective_to_injn.con
-cic:/matita/nat/permutation/injective_invert_permut.con
-cic:/matita/nat/permutation/inj_transpose.con
-cic:/matita/nat/permutation/f_invert_permut.con
-cic:/matita/nat/permutation/eq_transpose.con
-cic:/matita/nat/permutation/eq_to_bijn.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose_l.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose_i_Si.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose2.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose1.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose.con
-cic:/matita/nat/permutation/eq_map_iter_i_sigma.con
-cic:/matita/nat/permutation/eq_map_iter_i_pi.con
-cic:/matita/nat/permutation/eq_map_iter_i_fact.con
-cic:/matita/nat/permutation/eq_map_iter_i.con
-cic:/matita/nat/permutation/bijn_transpose_r.con
-cic:/matita/nat/permutation/bijn_transpose_l.con
-cic:/matita/nat/permutation/bijn_transpose.con
-cic:/matita/nat/permutation/bijn_n_Sn.con
-cic:/matita/nat/permutation/bijn_fg.con
-cic:/matita/nat/permutation/bijn_Sn_n.con
-cic:/matita/nat/permutation/bijn.con
-cic:/matita/nat/pi_p/true_to_pi_p_Sn.con
-cic:/matita/nat/pi_p/times_pi_p.con
-cic:/matita/nat/pi_p/pi_p_times.con
-cic:/matita/nat/pi_p/pi_p_pi_p1.con
-cic:/matita/nat/pi_p/pi_p_pi_p.con
-cic:/matita/nat/pi_p/pi_p_knm.con
-cic:/matita/nat/pi_p/pi_p_gi.con
-cic:/matita/nat/pi_p/pi_p_false.con
-cic:/matita/nat/pi_p/pi_p_SO.con
-cic:/matita/nat/pi_p/pi_p2.con
-cic:/matita/nat/pi_p/pi_p2'.con
-cic:/matita/nat/pi_p/pi_p.con
-cic:/matita/nat/pi_p/or_false_eq_SO_to_eq_pi_p.con
-cic:/matita/nat/pi_p/le_pi_p.con
-cic:/matita/nat/pi_p/false_to_pi_p_Sn.con
-cic:/matita/nat/pi_p/false_to_eq_pi_p.con
-cic:/matita/nat/pi_p/exp_times_pi_p.con
-cic:/matita/nat/pi_p/exp_sigma_p1.con
-cic:/matita/nat/pi_p/exp_sigma_p.con
-cic:/matita/nat/pi_p/exp_pi_p.con
-cic:/matita/nat/pi_p/eq_pi_p_gh.con
-cic:/matita/nat/pi_p/eq_pi_p1.con
-cic:/matita/nat/pi_p/eq_pi_p.con
-cic:/matita/nat/plus/sym_plus.con
-cic:/matita/nat/plus/plus_n_Sm.con
-cic:/matita/nat/plus/plus_n_SO.con
-cic:/matita/nat/plus/plus_n_O.con
-cic:/matita/nat/plus/plus.con
-cic:/matita/nat/plus/injective_plus_r.con
-cic:/matita/nat/plus/injective_plus_l.con
-cic:/matita/nat/plus/inj_plus_r.con
-cic:/matita/nat/plus/inj_plus_l.con
-cic:/matita/nat/plus/associative_plus.con
-cic:/matita/nat/plus/assoc_plus.con
-cic:/matita/nat/primes/transitive_divides.con
-cic:/matita/nat/primes/trans_divides.con
-cic:/matita/nat/primes/smallest_factor.con
-cic:/matita/nat/primes/reflexive_divides.con
-cic:/matita/nat/primes/primeb_true_to_prime.con
-cic:/matita/nat/primes/primeb_to_Prop.con
-cic:/matita/nat/primes/primeb_false_to_not_prime.con
-cic:/matita/nat/primes/primeb.con
-cic:/matita/nat/primes/prime_to_smallest_factor.con
-cic:/matita/nat/primes/prime_to_primeb_true.con
-cic:/matita/nat/primes/prime_to_lt_SO.con
-cic:/matita/nat/primes/prime_to_lt_O.con
-cic:/matita/nat/primes/prime_smallest_factor_n.con
-cic:/matita/nat/primes/prime.con
-cic:/matita/nat/primes/or_div_mod1.con
-cic:/matita/nat/primes/not_prime_to_primeb_false.con
-cic:/matita/nat/primes/not_prime_SO.con
-cic:/matita/nat/primes/not_prime_O.con
-cic:/matita/nat/primes/not_divides_to_divides_b_false.con
-cic:/matita/nat/primes/not_divides_S_fact.con
-cic:/matita/nat/primes/mod_S_fact.con
-cic:/matita/nat/primes/mod_O_to_divides.con
-cic:/matita/nat/primes/lt_smallest_factor_to_not_divides.con
-cic:/matita/nat/primes/lt_SO_smallest_factor.con
-cic:/matita/nat/primes/lt_O_smallest_factor.con
-cic:/matita/nat/primes/le_smallest_factor_n.con
-cic:/matita/nat/primes/eq_mod_to_divides.con
-cic:/matita/nat/primes/eq_div_plus.con
-cic:/matita/nat/primes/divides_to_mod_O.con
-cic:/matita/nat/primes/divides_to_lt_O.con
-cic:/matita/nat/primes/divides_to_le.con
-cic:/matita/nat/primes/divides_to_eq_times_div_div_times.con
-cic:/matita/nat/primes/divides_to_divides_b_true1.con
-cic:/matita/nat/primes/divides_to_divides_b_true.con
-cic:/matita/nat/primes/divides_to_div_mod_spec.con
-cic:/matita/nat/primes/divides_to_div.con
-cic:/matita/nat/primes/divides_times.con
-cic:/matita/nat/primes/divides_smallest_factor_n.con
-cic:/matita/nat/primes/divides_plus.con
-cic:/matita/nat/primes/divides_n_n.con
-cic:/matita/nat/primes/divides_n_O.con
-cic:/matita/nat/primes/divides_minus.con
-cic:/matita/nat/primes/divides_ind.con
-cic:/matita/nat/primes/divides_fact.con
-cic:/matita/nat/primes/divides_f_pi_f.con
-cic:/matita/nat/primes/divides_div.con
-cic:/matita/nat/primes/divides_b_true_to_lt_O.con
-cic:/matita/nat/primes/divides_b_true_to_divides1.con
-cic:/matita/nat/primes/divides_b_true_to_divides.con
-cic:/matita/nat/primes/divides_b_to_Prop.con
-cic:/matita/nat/primes/divides_b_false_to_not_divides1.con
-cic:/matita/nat/primes/divides_b_false_to_not_divides.con
-cic:/matita/nat/primes/divides_b_div_true.con
-cic:/matita/nat/primes/divides_b.con
-cic:/matita/nat/primes/divides_SO_n.con
-cic:/matita/nat/primes/divides.ind
-cic:/matita/nat/primes/div_mod_spec_to_divides.con
-cic:/matita/nat/primes/div_div.con
-cic:/matita/nat/primes/decidable_prime.con
-cic:/matita/nat/primes/decidable_divides.con
-cic:/matita/nat/primes/antisymmetric_divides.con
-cic:/matita/nat/relevant_equations/times_plus_plus.con
-cic:/matita/nat/relevant_equations/times_plus_l.con
-cic:/matita/nat/relevant_equations/times_minus_l.con
-cic:/matita/nat/relevant_equations/eq_pred_to_eq.con
-cic:/matita/nat/sigma_and_pi/sigma.con
-cic:/matita/nat/sigma_and_pi/pi.con
-cic:/matita/nat/sigma_and_pi/exp_pi_l.con
-cic:/matita/nat/sigma_and_pi/eq_sigma.con
-cic:/matita/nat/sigma_and_pi/eq_pi.con
-cic:/matita/nat/sigma_and_pi/eq_fact_pi.con
-cic:/matita/nat/sqrt/sqrt.con
-cic:/matita/nat/sqrt/monotonic_sqrt.con
-cic:/matita/nat/sqrt/lt_sqrt_to_le_times_l.con
-cic:/matita/nat/sqrt/lt_sqrt_n.con
-cic:/matita/nat/sqrt/lt_sqrt.con
-cic:/matita/nat/sqrt/leq_sqrt_n.con
-cic:/matita/nat/sqrt/le_sqrt_to_le_times_r.con
-cic:/matita/nat/sqrt/le_sqrt_to_le_times_l.con
-cic:/matita/nat/sqrt/le_sqrt_nl.con
-cic:/matita/nat/sqrt/le_sqrt_n_n.con
-cic:/matita/nat/sqrt/le_sqrt_n1.con
-cic:/matita/nat/sqrt/le_sqrt_log_n.con
-cic:/matita/nat/sqrt/eq_sqrt.con
-cic:/matita/nat/times/times_n_Sm.con
-cic:/matita/nat/times/times_n_SO.con
-cic:/matita/nat/times/times_n_O.con
-cic:/matita/nat/times/times_SSO_n.con
-cic:/matita/nat/times/times_SSO.con
-cic:/matita/nat/times/times_O_to_O.con
-cic:/matita/nat/times/times.con
-cic:/matita/nat/times/symmetric_times.con
-cic:/matita/nat/times/sym_times.con
-cic:/matita/nat/times/or_eq_eq_S.con
-cic:/matita/nat/times/distributive_times_plus.con
-cic:/matita/nat/times/distr_times_plus.con
-cic:/matita/nat/times/associative_times.con
-cic:/matita/nat/times/assoc_times.con
-cic:/matita/nat/totient/totient_times.con
-cic:/matita/nat/totient/totient.con
-cic:/matita/nat/totient1/sigma_p_Sn_divides_b_totient_n.con
-cic:/matita/nat/totient1/lt_O_to_divides_to_lt_O_div.con
cic:/matita/algebra/CoRN/SemiGroups/subcrr.con
cic:/matita/algebra/CoRN/SemiGroups/plus_assoc_unfolded.con
cic:/matita/algebra/CoRN/SemiGroups/plus_assoc.con
cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_is_CSemiGroup.con
cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_ind.con
cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup.ind
+cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
+cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
cic:/matita/algebra/CoRN/SetoidFun/total_eq_part.con
cic:/matita/algebra/CoRN/SetoidFun/ta_apfun.con
cic:/matita/algebra/CoRN/SetoidFun/sym_apfun.con
cic:/matita/algebra/CoRN/SetoidFun/inj2.con
cic:/matita/algebra/CoRN/SetoidFun/inj1.con
cic:/matita/algebra/CoRN/SetoidFun/id_is_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
cic:/matita/algebra/CoRN/SetoidFun/extension_wd.con
cic:/matita/algebra/CoRN/SetoidFun/extend.con
cic:/matita/algebra/CoRN/SetoidFun/ext2_a.con
cic:/matita/algebra/CoRN/SetoidFun/bijective.con
cic:/matita/algebra/CoRN/SetoidFun/bdom_wd.con
cic:/matita/algebra/CoRN/SetoidFun/assoc_comp.con
+cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
+cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/appA.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
+cic:/matita/algebra/CoRN/SetoidFun/UR.con
+cic:/matita/algebra/CoRN/SetoidFun/UQ.con
+cic:/matita/algebra/CoRN/SetoidFun/UP.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
+cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/Inv.con
+cic:/matita/algebra/CoRN/SetoidFun/Fid.con
+cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
+cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
+cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/BR.con
+cic:/matita/algebra/CoRN/SetoidFun/BQ.con
+cic:/matita/algebra/CoRN/SetoidFun/BP.con
+cic:/matita/algebra/CoRN/SetoidFun/Astar.con
cic:/matita/algebra/CoRN/SetoidInc/included_trans.con
cic:/matita/algebra/CoRN/SetoidInc/included_refl.con
cic:/matita/algebra/CoRN/SetoidInc/included_extend.con
cic:/matita/algebra/semigroups/Magma_rec.con
cic:/matita/algebra/semigroups/Magma_ind.con
cic:/matita/algebra/semigroups/Magma.ind
+cic:/matita/datatypes/bool/true_to_true_to_andb_true.con
+cic:/matita/datatypes/bool/orb_sym.con
+cic:/matita/datatypes/bool/orb_elim.con
+cic:/matita/datatypes/bool/orb.con
+cic:/matita/datatypes/bool/notb_notb.con
+cic:/matita/datatypes/bool/notb_elim.con
+cic:/matita/datatypes/bool/notb.con
+cic:/matita/datatypes/bool/not_eq_true_false.con
+cic:/matita/datatypes/bool/injective_notb.con
+cic:/matita/datatypes/bool/if_then_else.con
+cic:/matita/datatypes/bool/bool_to_decidable_eq.con
+cic:/matita/datatypes/bool/bool_rect.con
+cic:/matita/datatypes/bool/bool_rec.con
+cic:/matita/datatypes/bool/bool_ind.con
+cic:/matita/datatypes/bool/bool_elim.con
+cic:/matita/datatypes/bool/bool.ind
+cic:/matita/datatypes/bool/andb_true_true_r.con
+cic:/matita/datatypes/bool/andb_true_true.con
+cic:/matita/datatypes/bool/andb_sym.con
+cic:/matita/datatypes/bool/andb_elim.con
+cic:/matita/datatypes/bool/andb_assoc.con
+cic:/matita/datatypes/bool/andb.con
+cic:/matita/datatypes/bool/and_true.con
+cic:/matita/datatypes/bool/P_x_to_P_x_to_eq.con
+cic:/matita/datatypes/compare/compare_rect.con
+cic:/matita/datatypes/compare/compare_rec.con
+cic:/matita/datatypes/compare/compare_invert.con
+cic:/matita/datatypes/compare/compare_ind.con
+cic:/matita/datatypes/compare/compare.ind
+cic:/matita/datatypes/constructors/void_rect.con
+cic:/matita/datatypes/constructors/void_rec.con
+cic:/matita/datatypes/constructors/void_ind.con
+cic:/matita/datatypes/constructors/void.ind
+cic:/matita/datatypes/constructors/unit_rect.con
+cic:/matita/datatypes/constructors/unit_rec.con
+cic:/matita/datatypes/constructors/unit_ind.con
+cic:/matita/datatypes/constructors/unit.ind
+cic:/matita/datatypes/constructors/snd.con
+cic:/matita/datatypes/constructors/option_rect.con
+cic:/matita/datatypes/constructors/option_rec.con
+cic:/matita/datatypes/constructors/option_ind.con
+cic:/matita/datatypes/constructors/option.ind
+cic:/matita/datatypes/constructors/fst.con
+cic:/matita/datatypes/constructors/eq_pair_fst_snd.con
+cic:/matita/datatypes/constructors/Sum_rect.con
+cic:/matita/datatypes/constructors/Sum_rec.con
+cic:/matita/datatypes/constructors/Sum_ind.con
+cic:/matita/datatypes/constructors/Sum.ind
+cic:/matita/datatypes/constructors/Prod_rect.con
+cic:/matita/datatypes/constructors/Prod_rec.con
+cic:/matita/datatypes/constructors/Prod_ind.con
+cic:/matita/datatypes/constructors/Prod.ind
+cic:/matita/decidable_kit/decidable/reflect_rect.con
+cic:/matita/decidable_kit/decidable/reflect_rec.con
+cic:/matita/decidable_kit/decidable/reflect_inv.con
+cic:/matita/decidable_kit/decidable/reflect_ind.con
+cic:/matita/decidable_kit/decidable/reflect.ind
+cic:/matita/decidable_kit/decidable/prove_reflect.con
+cic:/matita/decidable_kit/decidable/p2bT.con
+cic:/matita/decidable_kit/decidable/p2bF.con
+cic:/matita/decidable_kit/decidable/orbP.con
+cic:/matita/decidable_kit/decidable/orbC.con
+cic:/matita/decidable_kit/decidable/orb.con
+cic:/matita/decidable_kit/decidable/negbP.con
+cic:/matita/decidable_kit/decidable/negb.con
+cic:/matita/decidable_kit/decidable/ltb_refl.con
+cic:/matita/decidable_kit/decidable/ltb_n_Sm.con
+cic:/matita/decidable_kit/decidable/ltbW.con
+cic:/matita/decidable_kit/decidable/ltbP.con
+cic:/matita/decidable_kit/decidable/ltb.con
+cic:/matita/decidable_kit/decidable/ltW.con
+cic:/matita/decidable_kit/decidable/ltS.con
+cic:/matita/decidable_kit/decidable/ltS'.con
+cic:/matita/decidable_kit/decidable/leb_refl.con
+cic:/matita/decidable_kit/decidable/leb_eqb.con
+cic:/matita/decidable_kit/decidable/lebW.con
+cic:/matita/decidable_kit/decidable/lebP.con
+cic:/matita/decidable_kit/decidable/idP.con
+cic:/matita/decidable_kit/decidable/eq_to_bool.con
+cic:/matita/decidable_kit/decidable/congr_S.con
+cic:/matita/decidable_kit/decidable/bool_to_eq.con
+cic:/matita/decidable_kit/decidable/b2pT.con
+cic:/matita/decidable_kit/decidable/b2pF.con
+cic:/matita/decidable_kit/decidable/andbPF.con
+cic:/matita/decidable_kit/decidable/andbP.con
+cic:/matita/decidable_kit/decidable/andb.con
+cic:/matita/decidable_kit/eqtype/test_canonical_option_eqType.con
+cic:/matita/decidable_kit/eqtype/sval.con
+cic:/matita/decidable_kit/eqtype/sub_eqType.con
+cic:/matita/decidable_kit/eqtype/sprop.con
+cic:/matita/decidable_kit/eqtype/sort_OF_nat.con
+cic:/matita/decidable_kit/eqtype/sort_OF_bool.con
+cic:/matita/decidable_kit/eqtype/sort.con
+cic:/matita/decidable_kit/eqtype/sigma_rect.con
+cic:/matita/decidable_kit/eqtype/sigma_rec.con
+cic:/matita/decidable_kit/eqtype/sigma_ind.con
+cic:/matita/decidable_kit/eqtype/sigma_eq_dec.con
+cic:/matita/decidable_kit/eqtype/sigma.ind
+cic:/matita/decidable_kit/eqtype/option_eqType.con
+cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con
+cic:/matita/decidable_kit/eqtype/ocmpP.con
+cic:/matita/decidable_kit/eqtype/ocmp.con
+cic:/matita/decidable_kit/eqtype/nat_eqType.con
+cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con
+cic:/matita/decidable_kit/eqtype/in_sub_rect.con
+cic:/matita/decidable_kit/eqtype/in_sub_rec.con
+cic:/matita/decidable_kit/eqtype/in_sub_inv.con
+cic:/matita/decidable_kit/eqtype/in_sub_ind.con
+cic:/matita/decidable_kit/eqtype/in_sub_eq.con
+cic:/matita/decidable_kit/eqtype/in_sub.ind
+cic:/matita/decidable_kit/eqtype/if_p.con
+cic:/matita/decidable_kit/eqtype/eqbP.con
+cic:/matita/decidable_kit/eqtype/eq_compatible.con
+cic:/matita/decidable_kit/eqtype/eqType_rect.con
+cic:/matita/decidable_kit/eqtype/eqType_rec.con
+cic:/matita/decidable_kit/eqtype/eqType_ind.con
+cic:/matita/decidable_kit/eqtype/eqType_decidable.con
+cic:/matita/decidable_kit/eqtype/eqType.ind
+cic:/matita/decidable_kit/eqtype/eqP.con
+cic:/matita/decidable_kit/eqtype/cmp_refl.con
+cic:/matita/decidable_kit/eqtype/cmpP.con
+cic:/matita/decidable_kit/eqtype/cmpC.con
+cic:/matita/decidable_kit/eqtype/cmp.con
+cic:/matita/decidable_kit/eqtype/bool_eqType.con
+cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con
+cic:/matita/decidable_kit/eqtype/bcmpP.con
+cic:/matita/decidable_kit/eqtype/bcmp.con
+cic:/matita/decidable_kit/fgraph/uniq_infgraphseq.con
+cic:/matita/decidable_kit/fgraph/setA.con
+cic:/matita/decidable_kit/fgraph/orb_refl.con
+cic:/matita/decidable_kit/fgraph/multss.con
+cic:/matita/decidable_kit/fgraph/multes.con
+cic:/matita/decidable_kit/fgraph/mkpermr.con
+cic:/matita/decidable_kit/fgraph/mem_multss.con
+cic:/matita/decidable_kit/fgraph/mem_multes.con
+cic:/matita/decidable_kit/fgraph/mem_mkpermr_size.con
+cic:/matita/decidable_kit/fgraph/mem_infgraphseq.con
+cic:/matita/decidable_kit/fgraph/mem_concat.con
+cic:/matita/decidable_kit/fgraph/iter.con
+cic:/matita/decidable_kit/fgraph/infgraphseq.con
+cic:/matita/decidable_kit/fgraph/infgraph_spec_rect.con
+cic:/matita/decidable_kit/fgraph/infgraph_spec_rec.con
+cic:/matita/decidable_kit/fgraph/infgraph_spec_inv.con
+cic:/matita/decidable_kit/fgraph/infgraph_spec_ind.con
+cic:/matita/decidable_kit/fgraph/infgraph_spec.ind
+cic:/matita/decidable_kit/fgraph/infgraphP.con
+cic:/matita/decidable_kit/fgraph/infgraph.con
+cic:/matita/decidable_kit/fgraph/fval_eqE.con
+cic:/matita/decidable_kit/fgraph/fval.con
+cic:/matita/decidable_kit/fgraph/fproof.con
+cic:/matita/decidable_kit/fgraph/fgraph_eqType.con
+cic:/matita/decidable_kit/fgraph/fgraph_eqP.con
+cic:/matita/decidable_kit/fgraph/fgraph_default.con
+cic:/matita/decidable_kit/fgraph/fgraphType_rect.con
+cic:/matita/decidable_kit/fgraph/fgraphType_rec.con
+cic:/matita/decidable_kit/fgraph/fgraphType_ind.con
+cic:/matita/decidable_kit/fgraph/fgraphType.ind
+cic:/matita/decidable_kit/fgraph/count_setA.con
+cic:/matita/decidable_kit/fintype/uniq_tail.con
+cic:/matita/decidable_kit/fintype/uniq_mem.con
+cic:/matita/decidable_kit/fintype/uniq_fintype_enum.con
+cic:/matita/decidable_kit/fintype/uniqP.con
+cic:/matita/decidable_kit/fintype/uniq.con
+cic:/matita/decidable_kit/fintype/sub_finType.con
+cic:/matita/decidable_kit/fintype/sub_enumP.con
+cic:/matita/decidable_kit/fintype/segment_finType.con
+cic:/matita/decidable_kit/fintype/segment_enum.con
+cic:/matita/decidable_kit/fintype/segment.con
+cic:/matita/decidable_kit/fintype/mem_finType.con
+cic:/matita/decidable_kit/fintype/mem_filter.con
+cic:/matita/decidable_kit/fintype/is_some.con
+cic:/matita/decidable_kit/fintype/iota_ltb.con
+cic:/matita/decidable_kit/fintype/fsort.con
+cic:/matita/decidable_kit/fintype/finType_rect.con
+cic:/matita/decidable_kit/fintype/finType_rec.con
+cic:/matita/decidable_kit/fintype/finType_ind.con
+cic:/matita/decidable_kit/fintype/finType.ind
+cic:/matita/decidable_kit/fintype/filter.con
+cic:/matita/decidable_kit/fintype/enum_uniq.con
+cic:/matita/decidable_kit/fintype/enum.con
+cic:/matita/decidable_kit/fintype/count_O_mem.con
+cic:/matita/decidable_kit/fintype/count_O.con
+cic:/matita/decidable_kit/fintype/andbC.con
+cic:/matita/decidable_kit/fintype/andbA.con
+cic:/matita/decidable_kit/fintype/Type_OF_finType.con
+cic:/matita/decidable_kit/list_aux/mem.con
+cic:/matita/decidable_kit/list_aux/list_eqType.con
+cic:/matita/decidable_kit/list_aux/lcmp_length.con
+cic:/matita/decidable_kit/list_aux/lcmpP.con
+cic:/matita/decidable_kit/list_aux/lcmp.con
+cic:/matita/decidable_kit/list_aux/count.con
+cic:/matita/decidable_kit/streicher/stepH.con
+cic:/matita/decidable_kit/streicher/step.con
+cic:/matita/decidable_kit/streicher/pirrel.con
+cic:/matita/decidable_kit/streicher/nu_k.con
+cic:/matita/decidable_kit/streicher/nu_inv.con
+cic:/matita/decidable_kit/streicher/nu.con
+cic:/matita/decidable_kit/streicher/decT.con
+cic:/matita/decidable_kit/streicher/cancel_nu_nu_inv.con
+cic:/matita/decidable_kit/streicher/cancel.con
cic:/matita/demo/power_derivative/monomio_product.con
cic:/matita/demo/power_derivative/monomio.con
cic:/matita/demo/power_derivative/inj.con
cic:/matita/demo/propositional_sequent_calculus/or_of_list.con
cic:/matita/demo/propositional_sequent_calculus/not_nf_inv.con
cic:/matita/demo/propositional_sequent_calculus/not_nf_ind.con
+cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
cic:/matita/demo/propositional_sequent_calculus/not_nf.ind
cic:/matita/demo/propositional_sequent_calculus/not_eq_nil_append_cons.con
cic:/matita/demo/propositional_sequent_calculus/negate.con
cic:/matita/demo/propositional_sequent_calculus/eq_to_eq_mem.con
cic:/matita/demo/propositional_sequent_calculus/eq_plus_n_m_O_to_eq_m_O.con
cic:/matita/demo/propositional_sequent_calculus/eq_notb_notb_b_b.con
+cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con
+cic:/matita/demo/propositional_sequent_calculus/elim_not.con
+cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con
+cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con
+cic:/matita/demo/propositional_sequent_calculus/derive_inv.con
+cic:/matita/demo/propositional_sequent_calculus/derive_ind.con
+cic:/matita/demo/propositional_sequent_calculus/derive.ind
+cic:/matita/demo/propositional_sequent_calculus/demorgan2.con
+cic:/matita/demo/propositional_sequent_calculus/demorgan1.con
+cic:/matita/demo/propositional_sequent_calculus/daemon.con
+cic:/matita/demo/propositional_sequent_calculus/completeness_base.con
+cic:/matita/demo/propositional_sequent_calculus/associative_andb.con
+cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con
+cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con
+cic:/matita/demo/propositional_sequent_calculus/and_of_list.con
+cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con
+cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con
+cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con
+cic:/matita/demo/propositional_sequent_calculus/Formula.ind
+cic:/matita/demo/realisability/type_OF_SP.con
+cic:/matita/demo/realisability/true_impl_realized.con
+cic:/matita/demo/realisability/sigma_rect.con
+cic:/matita/demo/realisability/sigma_rec.con
+cic:/matita/demo/realisability/sigma_ind.con
+cic:/matita/demo/realisability/sigma.ind
+cic:/matita/demo/realisability/realized.con
+cic:/matita/demo/realisability/pi2.con
+cic:/matita/demo/realisability/pi1.con
+cic:/matita/demo/realisability/modr.con
+cic:/matita/demo/realisability/id_axiom.con
+cic:/matita/demo/realisability/extraction.con
+cic:/matita/demo/realisability/elim_abs.con
+cic:/matita/demo/realisability/cut.con
+cic:/matita/demo/realisability/correct2.con
+cic:/matita/demo/realisability/correct.con
+cic:/matita/demo/realisability/and_i.con
+cic:/matita/demo/realisability/SP_rect.con
+cic:/matita/demo/realisability/SP_rec.con
+cic:/matita/demo/realisability/SP_ind.con
+cic:/matita/demo/realisability/SP.ind
+cic:/matita/demo/realisability/Prop_OF_SP.con
+cic:/matita/higher_order_defs/functions/symmetric2.con
+cic:/matita/higher_order_defs/functions/symmetric.con
+cic:/matita/higher_order_defs/functions/surjective.con
+cic:/matita/higher_order_defs/functions/monotonic.con
+cic:/matita/higher_order_defs/functions/injective.con
+cic:/matita/higher_order_defs/functions/eq_f_g_h.con
+cic:/matita/higher_order_defs/functions/distributive2.con
+cic:/matita/higher_order_defs/functions/distributive.con
+cic:/matita/higher_order_defs/functions/compose.con
+cic:/matita/higher_order_defs/functions/associative.con
+cic:/matita/higher_order_defs/ordering/antisymmetric.con
+cic:/matita/higher_order_defs/relations/transitive.con
+cic:/matita/higher_order_defs/relations/tight_apart.con
+cic:/matita/higher_order_defs/relations/symmetric.con
+cic:/matita/higher_order_defs/relations/relation.con
+cic:/matita/higher_order_defs/relations/reflexive.con
+cic:/matita/higher_order_defs/relations/irreflexive.con
+cic:/matita/higher_order_defs/relations/cotransitive.con
+cic:/matita/higher_order_defs/relations/antisymmetric.con
+cic:/matita/list/in/not_in_list_nil.con
+cic:/matita/list/in/mem_true_to_in_list.con
+cic:/matita/list/in/mem.con
+cic:/matita/list/in/incl_A_A.con
+cic:/matita/list/in/incl.con
+cic:/matita/list/in/in_list_to_mem_true.con
+cic:/matita/list/in/in_list_to_in_list_append_r.con
+cic:/matita/list/in/in_list_to_in_list_append_l.con
+cic:/matita/list/in/in_list_tail.con
+cic:/matita/list/in/in_list_singleton_to_eq.con
+cic:/matita/list/in/in_list_inv.con
+cic:/matita/list/in/in_list_ind.con
+cic:/matita/list/in/in_list_filter_to_p_true.con
+cic:/matita/list/in/in_list_filter_r.con
+cic:/matita/list/in/in_list_filter.con
+cic:/matita/list/in/in_list_cons_case.con
+cic:/matita/list/in/in_list_append_to_or_in_list.con
+cic:/matita/list/in/in_list.ind
+cic:/matita/list/list/x3.con
+cic:/matita/list/list/x2.con
+cic:/matita/list/list/x1.con
+cic:/matita/list/list/tmp.con
+cic:/matita/list/list/tail.con
+cic:/matita/list/list/permutation_inv.con
+cic:/matita/list/list/permutation_ind.con
+cic:/matita/list/list/permutation.ind
+cic:/matita/list/list/permut1_inv.con
+cic:/matita/list/list/permut1_ind.con
+cic:/matita/list/list/nth.con
+cic:/matita/list/list/nil_cons.con
+cic:/matita/list/list/map.con
+cic:/matita/list/list/list_rect.con
+cic:/matita/list/list/list_rec.con
+cic:/matita/list/list/list_ind2.con
+cic:/matita/list/list/list_ind.con
+cic:/matita/list/list/list.ind
+cic:/matita/list/list/length.con
+cic:/matita/list/list/le_length_filter.con
+cic:/matita/list/list/iota.con
+cic:/matita/list/list/id_list.con
+cic:/matita/list/list/foldr.con
+cic:/matita/list/list/filter.con
+cic:/matita/list/list/eq_map.con
+cic:/matita/list/list/cons_append_commute.con
+cic:/matita/list/list/associative_append.con
+cic:/matita/list/list/append_nil.con
+cic:/matita/list/list/append_cons.con
+cic:/matita/list/list/append.con
+cic:/matita/list/sort/sorted_to_minimum.con
+cic:/matita/list/sort/sorted_to_eq_sorted_b_true.con
+cic:/matita/list/sort/sorted_inv.con
+cic:/matita/list/sort/sorted_ind.con
+cic:/matita/list/sort/sorted_cons_to_sorted.con
+cic:/matita/list/sort/sorted.ind
+cic:/matita/list/sort/ordered_injective.con
+cic:/matita/list/sort/ordered.con
+cic:/matita/list/sort/insertionsort_sorted.con
+cic:/matita/list/sort/insertionsort.con
+cic:/matita/list/sort/insert_sorted.con
+cic:/matita/list/sort/insert_ind.con
+cic:/matita/list/sort/insert.con
+cic:/matita/logic/coimplication/iff_trans.con
+cic:/matita/logic/coimplication/iff_sym.con
+cic:/matita/logic/coimplication/iff_refl.con
+cic:/matita/logic/coimplication/iff_intro.con
+cic:/matita/logic/coimplication/Iff.con
+cic:/matita/logic/connectives/proj2.con
+cic:/matita/logic/connectives/proj1.con
+cic:/matita/logic/connectives/iff.con
+cic:/matita/logic/connectives/ex_ind.con
+cic:/matita/logic/connectives/ex2_ind.con
+cic:/matita/logic/connectives/ex2.ind
+cic:/matita/logic/connectives/ex.ind
+cic:/matita/logic/connectives/decidable.con
+cic:/matita/logic/connectives/absurd.con
+cic:/matita/logic/connectives/True_rect.con
+cic:/matita/logic/connectives/True_rec.con
+cic:/matita/logic/connectives/True_ind.con
+cic:/matita/logic/connectives/True.ind
+cic:/matita/logic/connectives/Or_ind.con
+cic:/matita/logic/connectives/Or_ind'.con
+cic:/matita/logic/connectives/Or.ind
+cic:/matita/logic/connectives/Not.con
+cic:/matita/logic/connectives/False_rect.con
+cic:/matita/logic/connectives/False_rec.con
+cic:/matita/logic/connectives/False_ind.con
+cic:/matita/logic/connectives/False.ind
+cic:/matita/logic/connectives/And_rect.con
+cic:/matita/logic/connectives/And_rec.con
+cic:/matita/logic/connectives/And_ind.con
+cic:/matita/logic/connectives/And.ind
+cic:/matita/logic/connectives2/transitive_iff.con
+cic:/matita/logic/connectives2/symmetric_iff.con
+cic:/matita/logic/connectives2/reflexive_iff.con
+cic:/matita/logic/equality/transitive_eq.con
+cic:/matita/logic/equality/trans_sym_eq.con
+cic:/matita/logic/equality/trans_eq.con
+cic:/matita/logic/equality/symmetric_eq.con
+cic:/matita/logic/equality/sym_eq.con
+cic:/matita/logic/equality/reflexive_eq.con
+cic:/matita/logic/equality/nu_left_inv.con
+cic:/matita/logic/equality/nu_inv.con
+cic:/matita/logic/equality/nu_constant.con
+cic:/matita/logic/equality/nu.con
+cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con
+cic:/matita/logic/equality/eq_rect.con
+cic:/matita/logic/equality/eq_rect'.con
+cic:/matita/logic/equality/eq_rec.con
+cic:/matita/logic/equality/eq_ind.con
+cic:/matita/logic/equality/eq_f2.con
+cic:/matita/logic/equality/eq_f.con
+cic:/matita/logic/equality/eq_f'.con
+cic:/matita/logic/equality/eq_elim_r.con
+cic:/matita/logic/equality/eq_elim_r'.con
+cic:/matita/logic/equality/eq_elim_r''.con
+cic:/matita/logic/equality/eq_OF_eq2.con
+cic:/matita/logic/equality/eq_OF_eq1.con
+cic:/matita/logic/equality/eq_OF_eq.con
+cic:/matita/logic/equality/eq.ind
+cic:/matita/logic/equality/comp.con
+cic:/matita/nat/bertrand/tech3.con
+cic:/matita/nat/bertrand/tech1.con
+cic:/matita/nat/bertrand/tech.con
+cic:/matita/nat/bertrand/sorted_lt.con
+cic:/matita/nat/bertrand/sorted_list_n_aux.con
+cic:/matita/nat/bertrand/sorted_gt.con
+cic:/matita/nat/bertrand/sieve_sound2.con
+cic:/matita/nat/bertrand/sieve_sound1.con
+cic:/matita/nat/bertrand/sieve_sorted.con
+cic:/matita/nat/bertrand/sieve_prime.con
+cic:/matita/nat/bertrand/sieve_aux.con
+cic:/matita/nat/bertrand/sieve.con
+cic:/matita/nat/bertrand/not_not_bertrand_to_bertrand1.con
+cic:/matita/nat/bertrand/not_not_bertrand_to_bertrand.con
+cic:/matita/nat/bertrand/not_bertrand_to_le_B.con
+cic:/matita/nat/bertrand/not_bertrand_to_le2.con
+cic:/matita/nat/bertrand/not_bertrand_to_le1.con
+cic:/matita/nat/bertrand/not_bertrand.con
+cic:/matita/nat/bertrand/min_prim.con
+cic:/matita/nat/bertrand/lt_to_div_O.con
+cic:/matita/nat/bertrand/lt_div_to_times.con
+cic:/matita/nat/bertrand/lt_div_S_div.con
+cic:/matita/nat/bertrand/lprim.con
+cic:/matita/nat/bertrand/list_of_primes_to_bertrand.con
+cic:/matita/nat/bertrand/list_of_primes.con
+cic:/matita/nat/bertrand/list_n_aux.con
+cic:/matita/nat/bertrand/list_n.con
+cic:/matita/nat/bertrand/list_divides.con
+cic:/matita/nat/bertrand/le_to_bertrand2.con
+cic:/matita/nat/bertrand/le_to_bertrand.con
+cic:/matita/nat/bertrand/le_times_div_m_m.con
+cic:/matita/nat/bertrand/le_list_n_r.con
+cic:/matita/nat/bertrand/le_list_n_aux_r.con
+cic:/matita/nat/bertrand/le_list_n_aux_k_k.con
+cic:/matita/nat/bertrand/le_list_n_aux.con
+cic:/matita/nat/bertrand/le_list_n.con
+cic:/matita/nat/bertrand/le_length_list_n.con
+cic:/matita/nat/bertrand/le_k.con
+cic:/matita/nat/bertrand/le_SSO_list_n.con
+cic:/matita/nat/bertrand/le_B_split2_exp.con
+cic:/matita/nat/bertrand/le_B_split1_teta.con
+cic:/matita/nat/bertrand/k1.con
+cic:/matita/nat/bertrand/k.con
+cic:/matita/nat/bertrand/in_list_sieve_to_prime.con
+cic:/matita/nat/bertrand/in_list_sieve_to_leq.con
+cic:/matita/nat/bertrand/in_list_SSO_list_n.con
+cic:/matita/nat/bertrand/exp_plus_SSO.con
+cic:/matita/nat/bertrand/eq_B_B1.con
+cic:/matita/nat/bertrand/eq_B1_times_B_split1_B_split2.con
+cic:/matita/nat/bertrand/divides_to_prime_divides.con
+cic:/matita/nat/bertrand/checker_sound.con
+cic:/matita/nat/bertrand/checker_cons.con
+cic:/matita/nat/bertrand/checker.con
+cic:/matita/nat/bertrand/check_list2.con
+cic:/matita/nat/bertrand/check_list1.con
+cic:/matita/nat/bertrand/check_list.con
+cic:/matita/nat/bertrand/bertrand_n.con
+cic:/matita/nat/bertrand/bertrand.con
+cic:/matita/nat/bertrand/B_split2.con
+cic:/matita/nat/bertrand/B_split1.con
+cic:/matita/nat/bertrand/B1.con
+cic:/matita/nat/binomial/lt_O_bc.con
+cic:/matita/nat/binomial/fact_minus.con
+cic:/matita/nat/binomial/exp_plus_sigma_p.con
+cic:/matita/nat/binomial/exp_Sn_SSO.con
+cic:/matita/nat/binomial/exp_S_sigma_p.con
+cic:/matita/nat/binomial/bc_n_n.con
+cic:/matita/nat/binomial/bc_n_O.con
+cic:/matita/nat/binomial/bc2.con
+cic:/matita/nat/binomial/bc1.con
+cic:/matita/nat/binomial/bc.con
+cic:/matita/nat/chebyshev/times_SSO_pred.con
+cic:/matita/nat/chebyshev/sigma_p_divides_b1.con
+cic:/matita/nat/chebyshev/sigma_p_divides_b.con
+cic:/matita/nat/chebyshev/prim.con
+cic:/matita/nat/chebyshev/pi_p_primeb_divides_b.con
+cic:/matita/nat/chebyshev/pi_p_primeb5.con
+cic:/matita/nat/chebyshev/pi_p_primeb4.con
+cic:/matita/nat/chebyshev/pi_p_primeb1.con
+cic:/matita/nat/chebyshev/pi_p_primeb.con
+cic:/matita/nat/chebyshev/not_prime_times_SSO.con
+cic:/matita/nat/chebyshev/monotonic_A.con
+cic:/matita/nat/chebyshev/lt_max_to_pi_p_primeb.con
+cic:/matita/nat/chebyshev/lt_SSSSO_to_le_B_exp.con
+cic:/matita/nat/chebyshev/lt_SSSSO_to_le_A_exp.con
+cic:/matita/nat/chebyshev/lt_SO_to_le_exp_B.con
+cic:/matita/nat/chebyshev/lt_SO_to_le_B_exp.con
+cic:/matita/nat/chebyshev/le_primr.con
+cic:/matita/nat/chebyshev/le_priml1.con
+cic:/matita/nat/chebyshev/le_priml.con
+cic:/matita/nat/chebyshev/le_prim_n3.con
+cic:/matita/nat/chebyshev/le_prim_n2.con
+cic:/matita/nat/chebyshev/le_prim_n1.con
+cic:/matita/nat/chebyshev/le_prim_n.con
+cic:/matita/nat/chebyshev/le_prim_log.con
+cic:/matita/nat/chebyshev/le_pred.con
+cic:/matita/nat/chebyshev/le_ord_log.con
+cic:/matita/nat/chebyshev/le_n_SSSSSSSSO_to_le_A_exp.con
+cic:/matita/nat/chebyshev/le_fact_A.con
+cic:/matita/nat/chebyshev/le_exp_primr.con
+cic:/matita/nat/chebyshev/le_exp_priml.con
+cic:/matita/nat/chebyshev/le_exp_prim4l.con
+cic:/matita/nat/chebyshev/le_exp_B.con
+cic:/matita/nat/chebyshev/le_S_times_SSO.con
+cic:/matita/nat/chebyshev/le_B_exp.con
+cic:/matita/nat/chebyshev/le_B_A4.con
+cic:/matita/nat/chebyshev/le_B_A.con
+cic:/matita/nat/chebyshev/le_Al1.con
+cic:/matita/nat/chebyshev/le_Al.con
+cic:/matita/nat/chebyshev/le_A_exp5.con
+cic:/matita/nat/chebyshev/le_A_exp4.con
+cic:/matita/nat/chebyshev/le_A_exp1.con
+cic:/matita/nat/chebyshev/le_A_exp.con
+cic:/matita/nat/chebyshev/le_A_BA1.con
+cic:/matita/nat/chebyshev/le_A_BA.con
+cic:/matita/nat/chebyshev/leA_r2.con
+cic:/matita/nat/chebyshev/leA_prim.con
+cic:/matita/nat/chebyshev/fact_pi_p3.con
+cic:/matita/nat/chebyshev/fact_pi_p2.con
+cic:/matita/nat/chebyshev/fact_pi_p.con
+cic:/matita/nat/chebyshev/exp_fact_SSO.con
+cic:/matita/nat/chebyshev/eq_sigma_pi_SO_n.con
+cic:/matita/nat/chebyshev/eq_sigma_p_div.con
+cic:/matita/nat/chebyshev/eq_prim_prim_pred.con
+cic:/matita/nat/chebyshev/eq_pi_p_primeb_divides_b.con
+cic:/matita/nat/chebyshev/eq_ord_sigma_p.con
+cic:/matita/nat/chebyshev/eq_fact_pi_p.con
+cic:/matita/nat/chebyshev/eq_fact_B.con
+cic:/matita/nat/chebyshev/eq_A_SSO_n.con
+cic:/matita/nat/chebyshev/eq_A_A'.con
+cic:/matita/nat/chebyshev/B_SSSSSSSSO.con
+cic:/matita/nat/chebyshev/B_SSSSSSSO.con
+cic:/matita/nat/chebyshev/B_SSSSSSO.con
+cic:/matita/nat/chebyshev/B_SSSSSO.con
+cic:/matita/nat/chebyshev/B_SSSSO.con
+cic:/matita/nat/chebyshev/B_SSSO.con
+cic:/matita/nat/chebyshev/B.con
+cic:/matita/nat/chebyshev/A_SSSSO.con
+cic:/matita/nat/chebyshev/A_SSSO.con
+cic:/matita/nat/chebyshev/A_SSO.con
+cic:/matita/nat/chebyshev/A_SO.con
+cic:/matita/nat/chebyshev/A.con
+cic:/matita/nat/chebyshev/A'.con
+cic:/matita/nat/chebyshev_teta/teta_pred.con
+cic:/matita/nat/chebyshev_teta/teta_pi_p_teta.con
+cic:/matita/nat/chebyshev_teta/teta.con
+cic:/matita/nat/chebyshev_teta/prime_to_divides_M.con
+cic:/matita/nat/chebyshev_teta/lt_O_to_le_teta_exp_teta.con
+cic:/matita/nat/chebyshev_teta/lt_O_teta.con
+cic:/matita/nat/chebyshev_teta/lt_M.con
+cic:/matita/nat/chebyshev_teta/le_teta_M_teta.con
+cic:/matita/nat/chebyshev_teta/le_teta.con
+cic:/matita/nat/chebyshev_teta/divides_pi_p_M1.con
+cic:/matita/nat/chebyshev_teta/divides_pi_p_M.con
+cic:/matita/nat/chebyshev_teta/divides_fact_to_le.con
+cic:/matita/nat/chebyshev_teta/divides_fact_to_divides.con
+cic:/matita/nat/chebyshev_teta/div_teta_teta.con
+cic:/matita/nat/chebyshev_teta/M.con
+cic:/matita/nat/chebyshev_thm/theta_pi.con
+cic:/matita/nat/chebyshev_thm/log_pi_p.con
+cic:/matita/nat/chebyshev_thm/le_log_C2_sigma_p.con
+cic:/matita/nat/chebyshev_thm/jj.con
+cic:/matita/nat/chebyshev_thm/daemon.con
+cic:/matita/nat/chebyshev_thm/asdasd.con
+cic:/matita/nat/chebyshev_thm/C2.con
+cic:/matita/nat/chebyshev_thm/C1.con
+cic:/matita/nat/chebyshev_thm/C.con
+cic:/matita/nat/chinese_reminder/mod_cr_pair.con
+cic:/matita/nat/chinese_reminder/cr_pair4.con
+cic:/matita/nat/chinese_reminder/cr_pair3.con
+cic:/matita/nat/chinese_reminder/cr_pair2.con
+cic:/matita/nat/chinese_reminder/cr_pair1.con
+cic:/matita/nat/chinese_reminder/cr_pair.con
+cic:/matita/nat/chinese_reminder/and_congruent_congruent_lt.con
+cic:/matita/nat/chinese_reminder/and_congruent_congruent.con
+cic:/matita/nat/compare/not_eq_to_eqb_false.con
+cic:/matita/nat/compare/nat_compare_to_Prop.con
+cic:/matita/nat/compare/nat_compare_pred_pred.con
+cic:/matita/nat/compare/nat_compare_n_n.con
+cic:/matita/nat/compare/nat_compare_n_m_m_n.con
+cic:/matita/nat/compare/nat_compare_elim.con
+cic:/matita/nat/compare/nat_compare_S_S.con
+cic:/matita/nat/compare/nat_compare.con
+cic:/matita/nat/compare/ltb_to_Prop.con
+cic:/matita/nat/compare/ltb_elim.con
+cic:/matita/nat/compare/ltb.con
+cic:/matita/nat/compare/lt_to_leb_false.con
+cic:/matita/nat/compare/leb_true_to_le.con
+cic:/matita/nat/compare/leb_to_Prop.con
+cic:/matita/nat/compare/leb_false_to_not_le.con
+cic:/matita/nat/compare/leb_elim.con
+cic:/matita/nat/compare/leb.con
+cic:/matita/nat/compare/le_to_leb_true.con
+cic:/matita/nat/compare/eqb_true_to_eq.con
+cic:/matita/nat/compare/eqb_to_Prop.con
+cic:/matita/nat/compare/eqb_n_n.con
+cic:/matita/nat/compare/eqb_false_to_not_eq.con
+cic:/matita/nat/compare/eqb_elim.con
+cic:/matita/nat/compare/eqb.con
+cic:/matita/nat/compare/eq_to_eqb_true.con
+cic:/matita/nat/congruence/transitive_congruent.con
+cic:/matita/nat/congruence/mod_times_mod.con
+cic:/matita/nat/congruence/mod_times.con
+cic:/matita/nat/congruence/mod_mod.con
+cic:/matita/nat/congruence/le_to_mod.con
+cic:/matita/nat/congruence/eq_times_plus_to_congruent.con
+cic:/matita/nat/congruence/divides_to_congruent.con
+cic:/matita/nat/congruence/congruent_to_divides.con
+cic:/matita/nat/congruence/congruent_times.con
+cic:/matita/nat/congruence/congruent_pi.con
+cic:/matita/nat/congruence/congruent_n_n.con
+cic:/matita/nat/congruence/congruent_n_mod_times.con
+cic:/matita/nat/congruence/congruent_n_mod_n.con
+cic:/matita/nat/congruence/congruent.con
+cic:/matita/nat/congruence/S_mod.con
+cic:/matita/nat/count/sigma_times.con
+cic:/matita/nat/count/sigma_plus1.con
+cic:/matita/nat/count/sigma_plus.con
+cic:/matita/nat/count/sigma_f_g.con
+cic:/matita/nat/count/eq_sigma_sigma1.con
+cic:/matita/nat/count/eq_sigma_sigma.con
+cic:/matita/nat/count/count_times.con
+cic:/matita/nat/count/count.con
+cic:/matita/nat/count/bool_to_nat_andb.con
+cic:/matita/nat/count/bool_to_nat.con
+cic:/matita/nat/div_and_mod/or_div_mod.con
+cic:/matita/nat/div_and_mod/n_divides_aux.con
+cic:/matita/nat/div_and_mod/n_divides.con
+cic:/matita/nat/div_and_mod/mod_plus_times.con
+cic:/matita/nat/div_and_mod/mod_n_n.con
+cic:/matita/nat/div_and_mod/mod_aux.con
+cic:/matita/nat/div_and_mod/mod_SO.con
+cic:/matita/nat/div_and_mod/mod_S.con
+cic:/matita/nat/div_and_mod/mod_O_n.con
+cic:/matita/nat/div_and_mod/mod.con
+cic:/matita/nat/div_and_mod/lt_to_eq_mod.con
+cic:/matita/nat/div_and_mod/lt_mod_m_m.con
+cic:/matita/nat/div_and_mod/lt_O_to_injective_times_r.con
+cic:/matita/nat/div_and_mod/lt_O_to_injective_times_l.con
+cic:/matita/nat/div_and_mod/lt_O_to_div_times.con
+cic:/matita/nat/div_and_mod/le_mod_aux_m_m.con
+cic:/matita/nat/div_and_mod/injective_times_r.con
+cic:/matita/nat/div_and_mod/injective_times_l.con
+cic:/matita/nat/div_and_mod/inj_times_r1.con
+cic:/matita/nat/div_and_mod/inj_times_r.con
+cic:/matita/nat/div_and_mod/inj_times_l1.con
+cic:/matita/nat/div_and_mod/inj_times_l.con
+cic:/matita/nat/div_and_mod/eq_times_div_minus_mod.con
+cic:/matita/nat/div_and_mod/eq_div_O.con
+cic:/matita/nat/div_and_mod/div_times.con
+cic:/matita/nat/div_and_mod/div_plus_times.con
+cic:/matita/nat/div_and_mod/div_n_n.con
+cic:/matita/nat/div_and_mod/div_mod_spec_to_not_eq_O.con
+cic:/matita/nat/div_and_mod/div_mod_spec_to_eq2.con
+cic:/matita/nat/div_and_mod/div_mod_spec_to_eq.con
+cic:/matita/nat/div_and_mod/div_mod_spec_times.con
+cic:/matita/nat/div_and_mod/div_mod_spec_rect.con
+cic:/matita/nat/div_and_mod/div_mod_spec_rec.con
+cic:/matita/nat/div_and_mod/div_mod_spec_ind.con
+cic:/matita/nat/div_and_mod/div_mod_spec_div_mod.con
+cic:/matita/nat/div_and_mod/div_mod_spec.ind
+cic:/matita/nat/div_and_mod/div_mod.con
+cic:/matita/nat/div_and_mod/div_aux_mod_aux.con
+cic:/matita/nat/div_and_mod/div_aux.con
+cic:/matita/nat/div_and_mod/div_SO.con
+cic:/matita/nat/div_and_mod/div.con
+cic:/matita/nat/div_and_mod_diseq/monotonic_div.con
+cic:/matita/nat/div_and_mod_diseq/lt_times_to_lt_div.con
+cic:/matita/nat/div_and_mod_diseq/lt_times_to_lt.con
+cic:/matita/nat/div_and_mod_diseq/lt_m_nm.con
+cic:/matita/nat/div_and_mod_diseq/lt_div_S.con
+cic:/matita/nat/div_and_mod_diseq/lt_div.con
+cic:/matita/nat/div_and_mod_diseq/le_times_to_le_div2.con
+cic:/matita/nat/div_and_mod_diseq/le_times_to_le_div.con
+cic:/matita/nat/div_and_mod_diseq/le_times_div_div_times.con
+cic:/matita/nat/div_and_mod_diseq/le_plus_mod.con
+cic:/matita/nat/div_and_mod_diseq/le_plus_div.con
+cic:/matita/nat/div_and_mod_diseq/le_div_times_m.con
+cic:/matita/nat/div_and_mod_diseq/le_div_times_Sm.con
+cic:/matita/nat/div_and_mod_diseq/le_div_plus_S.con
+cic:/matita/nat/div_and_mod_diseq/le_div_S_S_div.con
+cic:/matita/nat/div_and_mod_diseq/le_div.con
+cic:/matita/nat/euler_theorem/totient_card_aux.con
+cic:/matita/nat/euler_theorem/totient_card.con
+cic:/matita/nat/euler_theorem/permut_p_mod.con
+cic:/matita/nat/euler_theorem/gcd_pi_p.con
+cic:/matita/nat/euler_theorem/congruent_map_iter_p_times.con
+cic:/matita/nat/euler_theorem/congruent_exp_totient_SO.con
+cic:/matita/nat/euler_theorem/card_Sn.con
+cic:/matita/nat/exp/times_exp.con
+cic:/matita/nat/exp/monotonic_exp1.con
+cic:/matita/nat/exp/lt_m_exp_nm.con
+cic:/matita/nat/exp/lt_exp_to_lt1.con
+cic:/matita/nat/exp/lt_exp_to_lt.con
+cic:/matita/nat/exp/lt_exp1.con
+cic:/matita/nat/exp/lt_exp.con
+cic:/matita/nat/exp/lt_O_exp.con
+cic:/matita/nat/exp/le_exp_to_le1.con
+cic:/matita/nat/exp/le_exp_to_le.con
+cic:/matita/nat/exp/le_exp.con
+cic:/matita/nat/exp/injective_exp_r.con
+cic:/matita/nat/exp/inj_exp_r.con
+cic:/matita/nat/exp/exp_to_eq_O.con
+cic:/matita/nat/exp/exp_plus_times.con
+cic:/matita/nat/exp/exp_n_SO.con
+cic:/matita/nat/exp/exp_n_O.con
+cic:/matita/nat/exp/exp_exp_times.con
+cic:/matita/nat/exp/exp_SSO.con
+cic:/matita/nat/exp/exp_SO_n.con
+cic:/matita/nat/exp/exp.con
+cic:/matita/nat/factorial/lt_n_fact_n.con
+cic:/matita/nat/factorial/le_n_fact_n.con
+cic:/matita/nat/factorial/le_SSO_fact.con
+cic:/matita/nat/factorial/le_SO_fact.con
+cic:/matita/nat/factorial/fact.con
+cic:/matita/nat/factorial2/lt_SSSSO_to_fact.con
+cic:/matita/nat/factorial2/lt_O_to_fact1.con
+cic:/matita/nat/factorial2/lt_O_fact.con
+cic:/matita/nat/factorial2/le_fact_10.con
+cic:/matita/nat/factorial2/factS.con
+cic:/matita/nat/factorial2/fact3.con
+cic:/matita/nat/factorial2/fact2.con
+cic:/matita/nat/factorial2/fact1.con
+cic:/matita/nat/factorial2/exp_S.con
+cic:/matita/nat/factorial2/ab_times_cd.con
+cic:/matita/nat/factorization/p_ord_to_lt_max_prime_factor1.con
+cic:/matita/nat/factorization/p_ord_to_lt_max_prime_factor.con
+cic:/matita/nat/factorization/not_eq_nf_last_nf_cons.con
+cic:/matita/nat/factorization/not_eq_nf_cons_O_nf_cons.con
+cic:/matita/nat/factorization/not_divides_defactorize_aux.con
+cic:/matita/nat/factorization/nat_fact_rect.con
+cic:/matita/nat/factorization/nat_fact_rec.con
+cic:/matita/nat/factorization/nat_fact_ind.con
+cic:/matita/nat/factorization/nat_fact_all_rect.con
+cic:/matita/nat/factorization/nat_fact_all_rec.con
+cic:/matita/nat/factorization/nat_fact_all_ind.con
+cic:/matita/nat/factorization/nat_fact_all.ind
+cic:/matita/nat/factorization/nat_fact.ind
+cic:/matita/nat/factorization/max_prime_factor_to_not_p_ord_O.con
+cic:/matita/nat/factorization/max_prime_factor.con
+cic:/matita/nat/factorization/max_p_exponent.con
+cic:/matita/nat/factorization/max_p.con
+cic:/matita/nat/factorization/lt_max_prime_factor_to_not_divides.con
+cic:/matita/nat/factorization/lt_SO_max_prime.con
+cic:/matita/nat/factorization/lt_SO_defactorize_aux.con
+cic:/matita/nat/factorization/lt_O_defactorize_aux.con
+cic:/matita/nat/factorization/injective_defactorize_aux.con
+cic:/matita/nat/factorization/injective_defactorize.con
+cic:/matita/nat/factorization/factorize_defactorize.con
+cic:/matita/nat/factorization/factorize_aux.con
+cic:/matita/nat/factorization/factorize.con
+cic:/matita/nat/factorization/eq_p_max.con
+cic:/matita/nat/factorization/eq_defactorize_aux_to_eq.con
+cic:/matita/nat/factorization/divides_to_max_prime_factor1.con
+cic:/matita/nat/factorization/divides_to_max_prime_factor.con
+cic:/matita/nat/factorization/divides_max_prime_factor_n.con
+cic:/matita/nat/factorization/divides_max_p_defactorize.con
+cic:/matita/nat/factorization/defactorize_factorize.con
+cic:/matita/nat/factorization/defactorize_aux_factorize_aux.con
+cic:/matita/nat/factorization/defactorize_aux.con
+cic:/matita/nat/factorization/defactorize.con
+cic:/matita/nat/fermat_little_theorem/prime_to_not_divides_fact.con
+cic:/matita/nat/fermat_little_theorem/permut_mod.con
+cic:/matita/nat/fermat_little_theorem/permut_S_mod.con
+cic:/matita/nat/fermat_little_theorem/congruent_exp_pred_SO.con
+cic:/matita/nat/gcd/symmetric_gcd.con
+cic:/matita/nat/gcd/sym_gcd.con
+cic:/matita/nat/gcd/prime_to_gcd_SO.con
+cic:/matita/nat/gcd/lt_O_gcd.con
+cic:/matita/nat/gcd/le_gcd_times.con
+cic:/matita/nat/gcd/gcd_times_SO_to_gcd_SO.con
+cic:/matita/nat/gcd/gcd_n_times_nm.con
+cic:/matita/nat/gcd/gcd_n_n.con
+cic:/matita/nat/gcd/gcd_mod.con
+cic:/matita/nat/gcd/gcd_aux.con
+cic:/matita/nat/gcd/gcd_SO_to_lt_n.con
+cic:/matita/nat/gcd/gcd_SO_to_lt_O.con
+cic:/matita/nat/gcd/gcd_SO_to_divides_times_to_divides.con
+cic:/matita/nat/gcd/gcd_SO_n.con
+cic:/matita/nat/gcd/gcd_O_to_eq_O.con
+cic:/matita/nat/gcd/gcd_O_n.con
+cic:/matita/nat/gcd/gcd.con
+cic:/matita/nat/gcd/eq_minus_gcd_aux.con
+cic:/matita/nat/gcd/eq_minus_gcd.con
+cic:/matita/nat/gcd/eq_gcd_times_SO.con
+cic:/matita/nat/gcd/eq_gcd_SO_to_not_divides.con
+cic:/matita/nat/gcd/divides_to_divides_times.con
+cic:/matita/nat/gcd/divides_times_to_divides.con
+cic:/matita/nat/gcd/divides_times_gcd_aux.con
+cic:/matita/nat/gcd/divides_mod_to_divides.con
+cic:/matita/nat/gcd/divides_mod_gcd.con
+cic:/matita/nat/gcd/divides_mod.con
+cic:/matita/nat/gcd/divides_gcd_nm.con
+cic:/matita/nat/gcd/divides_gcd_n.con
+cic:/matita/nat/gcd/divides_gcd_mod.con
+cic:/matita/nat/gcd/divides_gcd_m.con
+cic:/matita/nat/gcd/divides_gcd_aux_mn.con
+cic:/matita/nat/gcd/divides_gcd_aux.con
+cic:/matita/nat/gcd/divides_exp_to_eq.con
+cic:/matita/nat/gcd/divides_exp_to_divides.con
+cic:/matita/nat/gcd/divides_d_times_gcd.con
+cic:/matita/nat/gcd/divides_d_gcd.con
+cic:/matita/nat/gcd_properties1/gcd_plus_times_gcd.con
+cic:/matita/nat/gcd_properties1/gcd_SO_to_eq_gcd_times_times_gcd_gcd.con
+cic:/matita/nat/gcd_properties1/gcd_SO_to_divides_to_divides_to_divides_times.con
+cic:/matita/nat/gcd_properties1/gcd1.con
+cic:/matita/nat/gcd_properties1/eq_gcd_times_times_times_gcd.con
+cic:/matita/nat/gcd_properties1/eq_gcd_gcd_minus.con
+cic:/matita/nat/gcd_properties1/eq_gcd_div_div_div_gcd.con
+cic:/matita/nat/gcd_properties1/divides_times_to_divides_div_gcd.con
+cic:/matita/nat/gcd_properties1/associative_nat_gcd.con
+cic:/matita/nat/generic_iter_p/true_to_iter_p_gen_Sn.con
+cic:/matita/nat/generic_iter_p/p_ord_times.con
+cic:/matita/nat/generic_iter_p/or_false_eq_baseA_to_eq_iter_p_gen.con
+cic:/matita/nat/generic_iter_p/mod_p_ord_times.con
+cic:/matita/nat/generic_iter_p/lt_times_to_lt_O.con
+cic:/matita/nat/generic_iter_p/iter_p_gen_plusA.con
+cic:/matita/nat/generic_iter_p/iter_p_gen_knm.con
+cic:/matita/nat/generic_iter_p/iter_p_gen_iter_p_gen.con
+cic:/matita/nat/generic_iter_p/iter_p_gen_gi.con
+cic:/matita/nat/generic_iter_p/iter_p_gen_false.con
+cic:/matita/nat/generic_iter_p/iter_p_gen_divides.con
+cic:/matita/nat/generic_iter_p/iter_p_gen_2_eq.con
+cic:/matita/nat/generic_iter_p/iter_p_gen2.con
+cic:/matita/nat/generic_iter_p/iter_p_gen2'.con
+cic:/matita/nat/generic_iter_p/iter_p_gen.con
+cic:/matita/nat/generic_iter_p/false_to_iter_p_gen_Sn.con
+cic:/matita/nat/generic_iter_p/false_to_eq_iter_p_gen.con
+cic:/matita/nat/generic_iter_p/eq_p_ord_times.con
+cic:/matita/nat/generic_iter_p/eq_iter_p_gen_pred.con
+cic:/matita/nat/generic_iter_p/eq_iter_p_gen_gh.con
+cic:/matita/nat/generic_iter_p/eq_iter_p_gen1.con
+cic:/matita/nat/generic_iter_p/eq_iter_p_gen.con
+cic:/matita/nat/generic_iter_p/div_p_ord_times.con
+cic:/matita/nat/generic_iter_p/distributive_times_plus_iter_p_gen.con
+cic:/matita/nat/iteration2/true_to_sigma_p_Sn.con
+cic:/matita/nat/iteration2/symmetricIntPlus.con
+cic:/matita/nat/iteration2/sigma_p_true.con
+cic:/matita/nat/iteration2/sigma_p_times.con
+cic:/matita/nat/iteration2/sigma_p_sigma_p.con
+cic:/matita/nat/iteration2/sigma_p_plus_1.con
+cic:/matita/nat/iteration2/sigma_p_plus.con
+cic:/matita/nat/iteration2/sigma_p_knm.con
+cic:/matita/nat/iteration2/sigma_p_gi.con
+cic:/matita/nat/iteration2/sigma_p_false.con
+cic:/matita/nat/iteration2/sigma_p_divides.con
+cic:/matita/nat/iteration2/sigma_p2_eq.con
+cic:/matita/nat/iteration2/sigma_p2.con
+cic:/matita/nat/iteration2/sigma_p2'.con
+cic:/matita/nat/iteration2/sigma_p.con
+cic:/matita/nat/iteration2/sigma_P_SO_to_sigma_p_true.con
+cic:/matita/nat/iteration2/or_false_to_eq_sigma_p.con
+cic:/matita/nat/iteration2/lt_sigma_p.con
+cic:/matita/nat/iteration2/le_sigma_p1.con
+cic:/matita/nat/iteration2/le_sigma_p.con
+cic:/matita/nat/iteration2/false_to_sigma_p_Sn.con
+cic:/matita/nat/iteration2/false_to_eq_sigma_p.con
+cic:/matita/nat/iteration2/eq_sigma_p_sigma_p_times2.con
+cic:/matita/nat/iteration2/eq_sigma_p_sigma_p_times1.con
+cic:/matita/nat/iteration2/eq_sigma_p_pred.con
+cic:/matita/nat/iteration2/eq_sigma_p_gh.con
+cic:/matita/nat/iteration2/eq_sigma_p1.con
+cic:/matita/nat/iteration2/eq_sigma_p.con
+cic:/matita/nat/iteration2/eq_map_iter_i_sigma_p_alwaysTrue.con
+cic:/matita/nat/iteration2/distributive_times_plus_sigma_p.con
+cic:/matita/nat/iteration2/bool_to_nat_to_eq_sigma_p.con
+cic:/matita/nat/le_arith/monotonic_le_times_r.con
+cic:/matita/nat/le_arith/monotonic_le_times_l.con
+cic:/matita/nat/le_arith/monotonic_le_plus_r.con
+cic:/matita/nat/le_arith/monotonic_le_plus_l.con
+cic:/matita/nat/le_arith/le_times_to_le.con
+cic:/matita/nat/le_arith/le_times_r.con
+cic:/matita/nat/le_arith/le_times_n.con
+cic:/matita/nat/le_arith/le_times_l.con
+cic:/matita/nat/le_arith/le_times.con
+cic:/matita/nat/le_arith/le_plus_to_le.con
+cic:/matita/nat/le_arith/le_plus_r.con
+cic:/matita/nat/le_arith/le_plus_n_r.con
+cic:/matita/nat/le_arith/le_plus_n.con
+cic:/matita/nat/le_arith/le_plus_l.con
+cic:/matita/nat/le_arith/le_plus.con
+cic:/matita/nat/le_arith/le_S_times_SSO.con
+cic:/matita/nat/le_arith/eq_plus_to_le.con
+cic:/matita/nat/le_arith/O_lt_const_to_le_times_const.con
+cic:/matita/nat/log/lt_to_log_O.con
+cic:/matita/nat/log/lt_log_n_n.con
+cic:/matita/nat/log/lt_exp_log.con
+cic:/matita/nat/log/lt_O_log.con
+cic:/matita/nat/log/log_times_l.con
+cic:/matita/nat/log/log_times1.con
+cic:/matita/nat/log/log_times.con
+cic:/matita/nat/log/log_n_n.con
+cic:/matita/nat/log/log_i_SSOn.con
+cic:/matita/nat/log/log_exp2.con
+cic:/matita/nat/log/log_exp1.con
+cic:/matita/nat/log/log_exp.con
+cic:/matita/nat/log/log_div.con
+cic:/matita/nat/log/log_SO.con
+cic:/matita/nat/log/log.con
+cic:/matita/nat/log/le_log_plus.con
+cic:/matita/nat/log/le_log_n_n.con
+cic:/matita/nat/log/le_log.con
+cic:/matita/nat/log/le_exp_log.con
+cic:/matita/nat/log/exp_n_O.con
+cic:/matita/nat/log/eq_log_exp.con
+cic:/matita/nat/lt_arith/times_mod.con
+cic:/matita/nat/lt_arith/nat_compare_times_l.con
+cic:/matita/nat/lt_arith/monotonic_to_injective.con
+cic:/matita/nat/lt_arith/monotonic_lt_times_variant.con
+cic:/matita/nat/lt_arith/monotonic_lt_times_r.con
+cic:/matita/nat/lt_arith/monotonic_lt_times_l.con
+cic:/matita/nat/lt_arith/monotonic_lt_plus_r.con
+cic:/matita/nat/lt_arith/monotonic_lt_plus_l.con
+cic:/matita/nat/lt_arith/lt_to_lt_to_eq_div_div_times_times.con
+cic:/matita/nat/lt_arith/lt_to_le_to_lt_times.con
+cic:/matita/nat/lt_arith/lt_to_le_times_to_lt_S_to_div.con
+cic:/matita/nat/lt_arith/lt_to_div_to_and_le_times_lt_S.con
+cic:/matita/nat/lt_arith/lt_times_to_lt_r.con
+cic:/matita/nat/lt_arith/lt_times_to_lt_l.con
+cic:/matita/nat/lt_arith/lt_times_to_lt_O.con
+cic:/matita/nat/lt_arith/lt_times_r1.con
+cic:/matita/nat/lt_arith/lt_times_r.con
+cic:/matita/nat/lt_arith/lt_times_plus_times.con
+cic:/matita/nat/lt_arith/lt_times_n_to_lt_r.con
+cic:/matita/nat/lt_arith/lt_times_n_to_lt.con
+cic:/matita/nat/lt_arith/lt_times_l1.con
+cic:/matita/nat/lt_arith/lt_times_l.con
+cic:/matita/nat/lt_arith/lt_times_eq_O.con
+cic:/matita/nat/lt_arith/lt_times.con
+cic:/matita/nat/lt_arith/lt_plus_to_lt_r.con
+cic:/matita/nat/lt_arith/lt_plus_to_lt_l.con
+cic:/matita/nat/lt_arith/lt_plus_r.con
+cic:/matita/nat/lt_arith/lt_plus_l.con
+cic:/matita/nat/lt_arith/lt_plus.con
+cic:/matita/nat/lt_arith/lt_div_n_m_n.con
+cic:/matita/nat/lt_arith/lt_O_times_S_S.con
+cic:/matita/nat/lt_arith/le_to_lt_to_plus_lt.con
+cic:/matita/nat/lt_arith/increasing_to_injective.con
+cic:/matita/nat/lt_arith/eq_mod_O_to_lt_O_div.con
+cic:/matita/nat/lt_arith/eq_div_div_div_times.con
+cic:/matita/nat/lt_arith/eq_div_div_div_div.con
+cic:/matita/nat/lt_arith/SSO_mod.con
+cic:/matita/nat/lt_arith/O_lt_times_to_O_lt.con
+cic:/matita/nat/map_iter_p/pi_p_S.con
+cic:/matita/nat/map_iter_p/pi_p.con
+cic:/matita/nat/map_iter_p/permut_p_transpose.con
+cic:/matita/nat/map_iter_p/permut_p_compose.con
+cic:/matita/nat/map_iter_p/permut_p_S_to_permut_p.con
+cic:/matita/nat/map_iter_p/permut_p_O.con
+cic:/matita/nat/map_iter_p/permut_p.con
+cic:/matita/nat/map_iter_p/map_iter_p_S_true.con
+cic:/matita/nat/map_iter_p/map_iter_p_S_false.con
+cic:/matita/nat/map_iter_p/map_iter_p_O.con
+cic:/matita/nat/map_iter_p/map_iter_p.con
+cic:/matita/nat/map_iter_p/lt_O_pi_p.con
+cic:/matita/nat/map_iter_p/extentional_eq_n_to_permut_p.con
+cic:/matita/nat/map_iter_p/extentional_eq_n.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose3.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose2.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose1.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p_permut.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p_k.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p_a.con
+cic:/matita/nat/map_iter_p/eq_map_iter_p.con
+cic:/matita/nat/map_iter_p/decidable_n2.con
+cic:/matita/nat/map_iter_p/decidable_n1.con
+cic:/matita/nat/map_iter_p/decidable_n.con
+cic:/matita/nat/map_iter_p/count_card1.con
+cic:/matita/nat/map_iter_p/count_card.con
+cic:/matita/nat/map_iter_p/card.con
+cic:/matita/nat/map_iter_p/a_times_pi_p.con
+cic:/matita/nat/minimization/min_aux_S.con
+cic:/matita/nat/minimization/min_aux_O_f.con
+cic:/matita/nat/minimization/min_aux.con
+cic:/matita/nat/minimization/min_O_f.con
+cic:/matita/nat/minimization/min.con
+cic:/matita/nat/minimization/max_spec_to_max.con
+cic:/matita/nat/minimization/max_spec.con
+cic:/matita/nat/minimization/max_f_g.con
+cic:/matita/nat/minimization/max_S_max.con
+cic:/matita/nat/minimization/max_O_f.con
+cic:/matita/nat/minimization/max_O.con
+cic:/matita/nat/minimization/max.con
+cic:/matita/nat/minimization/lt_min_aux_to_false.con
+cic:/matita/nat/minimization/lt_max_to_false.con
+cic:/matita/nat/minimization/le_to_le_max.con
+cic:/matita/nat/minimization/le_min_aux_r.con
+cic:/matita/nat/minimization/le_min_aux.con
+cic:/matita/nat/minimization/le_max_n.con
+cic:/matita/nat/minimization/le_max_f_max_g.con
+cic:/matita/nat/minimization/false_to_lt_max.con
+cic:/matita/nat/minimization/f_min_aux_true.con
+cic:/matita/nat/minimization/f_max_true.con
+cic:/matita/nat/minimization/f_m_to_le_max.con
+cic:/matita/nat/minimization/f_false_to_le_max.con
+cic:/matita/nat/minimization/exists_max_forall_false.con
+cic:/matita/nat/minimization/exists_forall_le.con
+cic:/matita/nat/minus/plus_to_minus.con
+cic:/matita/nat/minus/plus_minus_m_m.con
+cic:/matita/nat/minus/plus_minus.con
+cic:/matita/nat/minus/monotonic_le_minus_r.con
+cic:/matita/nat/minus/minus_to_plus.con
+cic:/matita/nat/minus/minus_pred_pred.con
+cic:/matita/nat/minus/minus_plus_m_m.con
+cic:/matita/nat/minus/minus_n_n.con
+cic:/matita/nat/minus/minus_n_O.con
+cic:/matita/nat/minus/minus_m_minus_mn.con
+cic:/matita/nat/minus/minus_le_S_minus_S.con
+cic:/matita/nat/minus/minus_le_O_to_le.con
+cic:/matita/nat/minus/minus_Sn_n.con
+cic:/matita/nat/minus/minus_Sn_m.con
+cic:/matita/nat/minus/minus_S_S.con
+cic:/matita/nat/minus/minus.con
+cic:/matita/nat/minus/lt_to_lt_O_minus.con
+cic:/matita/nat/minus/lt_plus_to_lt_minus.con
+cic:/matita/nat/minus/lt_minus_to_plus.con
+cic:/matita/nat/minus/lt_minus_to_lt_plus.con
+cic:/matita/nat/minus/lt_minus_r.con
+cic:/matita/nat/minus/lt_minus_m.con
+cic:/matita/nat/minus/lt_minus_l.con
+cic:/matita/nat/minus/lt_minus_S_n_to_le_minus_n.con
+cic:/matita/nat/minus/lt_O_minus_to_lt.con
+cic:/matita/nat/minus/le_plus_to_minus_r.con
+cic:/matita/nat/minus/le_plus_to_minus.con
+cic:/matita/nat/minus/le_minus_to_plus.con
+cic:/matita/nat/minus/le_minus_m.con
+cic:/matita/nat/minus/le_SO_minus.con
+cic:/matita/nat/minus/eq_plus_minus_minus_minus.con
+cic:/matita/nat/minus/eq_minus_plus_plus_minus.con
+cic:/matita/nat/minus/eq_minus_n_m_O.con
+cic:/matita/nat/minus/eq_minus_minus_minus_plus.con
+cic:/matita/nat/minus/eq_minus_S_pred.con
+cic:/matita/nat/minus/distributive_times_minus.con
+cic:/matita/nat/minus/distr_times_minus.con
+cic:/matita/nat/nat/pred_Sn.con
+cic:/matita/nat/nat/pred.con
+cic:/matita/nat/nat/not_zero.con
+cic:/matita/nat/nat/not_eq_n_Sn.con
+cic:/matita/nat/nat/not_eq_S.con
+cic:/matita/nat/nat/not_eq_O_S.con
+cic:/matita/nat/nat/nat_rect.con
+cic:/matita/nat/nat/nat_rec.con
+cic:/matita/nat/nat/nat_ind.con
+cic:/matita/nat/nat/nat_elim2.con
+cic:/matita/nat/nat/nat_case1.con
+cic:/matita/nat/nat/nat_case.con
+cic:/matita/nat/nat/nat.ind
+cic:/matita/nat/nat/injective_S.con
+cic:/matita/nat/nat/inj_S.con
+cic:/matita/nat/nat/decidable_eq_nat.con
+cic:/matita/nat/neper/sigma_p_log_div2.con
+cic:/matita/nat/neper/sigma_p_log_div1.con
+cic:/matita/nat/neper/sigma_p_log_div.con
+cic:/matita/nat/neper/sigma_p_div_exp.con
+cic:/matita/nat/neper/neper_sigma_p3.con
+cic:/matita/nat/neper/neper_sigma_p2.con
+cic:/matita/nat/neper/neper_sigma_p1.con
+cic:/matita/nat/neper/neper_monotonic.con
+cic:/matita/nat/neper/lt_exp_sigma_p_exp.con
+cic:/matita/nat/neper/lt_exp_Sn_n_SSSO.con
+cic:/matita/nat/neper/lt_exp_Sn_m_SSSO.con
+cic:/matita/nat/neper/lt_SO_to_lt_exp_Sn_n_SSSO.con
+cic:/matita/nat/neper/le_sigma_p_div_log_div_pred_log.con
+cic:/matita/nat/neper/le_log_exp_fact_sigma_p.con
+cic:/matita/nat/neper/le_log_exp_Sn_log_exp_n.con
+cic:/matita/nat/neper/le_log_div_sigma_p.con
+cic:/matita/nat/neper/le_fact_exp1.con
+cic:/matita/nat/neper/le_fact_exp.con
+cic:/matita/nat/neper/le_exp_sigma_p_exp.con
+cic:/matita/nat/neper/le_exp_div.con
+cic:/matita/nat/neper/le_exp_SSO_fact.con
+cic:/matita/nat/neper/le_SSO_neper.con
+cic:/matita/nat/neper/le_SSO_exp_neper.con
+cic:/matita/nat/neper/eq_fact_pi_p.con
+cic:/matita/nat/neper/eq_exp_pi_p.con
+cic:/matita/nat/neper/divides_times_to_eq.con
+cic:/matita/nat/neper/divides_times_to_divides_div.con
+cic:/matita/nat/neper/divides_sigma_p_to_eq.con
+cic:/matita/nat/neper/divides_pi_p_to_eq.con
+cic:/matita/nat/neper/divides_pi_p.con
+cic:/matita/nat/neper/divides_fact_fact.con
+cic:/matita/nat/nth_prime/smallest_factor_fact.con
+cic:/matita/nat/nth_prime/prime_to_nth_prime.con
+cic:/matita/nat/nth_prime/prime_nth_prime.con
+cic:/matita/nat/nth_prime/nth_prime.con
+cic:/matita/nat/nth_prime/lt_nth_prime_to_not_prime.con
+cic:/matita/nat/nth_prime/lt_nth_prime_n_nth_prime_Sn.con
+cic:/matita/nat/nth_prime/lt_n_nth_prime_n.con
+cic:/matita/nat/nth_prime/lt_SO_nth_prime_n.con
+cic:/matita/nat/nth_prime/lt_O_nth_prime_n.con
+cic:/matita/nat/nth_prime/injective_nth_prime.con
+cic:/matita/nat/nth_prime/increasing_nth_prime.con
+cic:/matita/nat/nth_prime/ex_prime.con
+cic:/matita/nat/nth_prime/ex_m_le_n_nth_prime_m.con
+cic:/matita/nat/o/lt_times_SSO_n_exp_SSO_n.con
+cic:/matita/nat/o/lt_exp_n_SSO_exp_SSO_n.con
+cic:/matita/nat/o/le_times_n_exp.con
+cic:/matita/nat/o/le_times_exp_n_SSO_exp_SSO_n.con
+cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con
+cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n1.con
+cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n.con
+cic:/matita/nat/ord/p_ord_to_not_eq_O.con
+cic:/matita/nat/ord/p_ord_to_exp1.con
+cic:/matita/nat/ord/p_ord_times.con
+cic:/matita/nat/ord/p_ord_p.con
+cic:/matita/nat/ord/p_ord_inv.con
+cic:/matita/nat/ord/p_ord_exp1.con
+cic:/matita/nat/ord/p_ord_exp.con
+cic:/matita/nat/ord/p_ord_aux_to_not_mod_O.con
+cic:/matita/nat/ord/p_ord_aux_to_exp.con
+cic:/matita/nat/ord/p_ord_aux_to_Prop1.con
+cic:/matita/nat/ord/p_ord_aux_to_Prop.con
+cic:/matita/nat/ord/p_ord_aux.con
+cic:/matita/nat/ord/p_ord_O_to_not_divides.con
+cic:/matita/nat/ord/p_ord.con
+cic:/matita/nat/ord/ord_times.con
+cic:/matita/nat/ord/ord_rem.con
+cic:/matita/nat/ord/ord_ord_rem.con
+cic:/matita/nat/ord/ord_exp.con
+cic:/matita/nat/ord/ord_O_to_not_divides.con
+cic:/matita/nat/ord/ord.con
+cic:/matita/nat/ord/not_ord_O_to_divides.con
+cic:/matita/nat/ord/not_divides_to_p_ord_O.con
+cic:/matita/nat/ord/not_divides_to_ord_O.con
+cic:/matita/nat/ord/not_divides_ord_rem.con
+cic:/matita/nat/ord/mod_p_ord_inv.con
+cic:/matita/nat/ord/lt_ord_rem.con
+cic:/matita/nat/ord/lt_O_ord_rem.con
+cic:/matita/nat/ord/fst_p_ord_times.con
+cic:/matita/nat/ord/exp_ord.con
+cic:/matita/nat/ord/eq_p_ord_inv.con
+cic:/matita/nat/ord/divides_to_p_ord.con
+cic:/matita/nat/ord/divides_to_ord.con
+cic:/matita/nat/ord/divides_to_not_ord_O.con
+cic:/matita/nat/ord/divides_to_le_ord.con
+cic:/matita/nat/ord/divides_to_divides_ord_rem.con
+cic:/matita/nat/ord/divides_ord_rem.con
+cic:/matita/nat/ord/div_p_ord_inv.con
+cic:/matita/nat/orders/transitive_lt.con
+cic:/matita/nat/orders/transitive_le.con
+cic:/matita/nat/orders/trans_lt.con
+cic:/matita/nat/orders/trans_le.con
+cic:/matita/nat/orders/not_lt_to_le.con
+cic:/matita/nat/orders/not_le_to_lt.con
+cic:/matita/nat/orders/not_le_Sn_n.con
+cic:/matita/nat/orders/not_le_Sn_O.con
+cic:/matita/nat/orders/not_eq_to_le_to_lt.con
+cic:/matita/nat/orders/nat_elim1.con
+cic:/matita/nat/orders/ltn_to_ltO.con
+cic:/matita/nat/orders/lt_to_not_le.con
+cic:/matita/nat/orders/lt_to_not_eq.con
+cic:/matita/nat/orders/lt_to_lt_S_S.con
+cic:/matita/nat/orders/lt_to_le_to_lt.con
+cic:/matita/nat/orders/lt_to_le.con
+cic:/matita/nat/orders/lt_pred.con
+cic:/matita/nat/orders/lt_n_m_to_not_lt_m_Sn.con
+cic:/matita/nat/orders/lt_S_to_lt.con
+cic:/matita/nat/orders/lt_S_to_le.con
+cic:/matita/nat/orders/lt_S_S_to_lt.con
+cic:/matita/nat/orders/lt_SO_n_to_lt_O_pred_n.con
+cic:/matita/nat/orders/lt_O_n_elim.con
+cic:/matita/nat/orders/lt_O_S.con
+cic:/matita/nat/orders/lt.con
+cic:/matita/nat/orders/le_to_or_lt_eq.con
+cic:/matita/nat/orders/le_to_not_lt.con
+cic:/matita/nat/orders/le_to_lt_to_lt.con
+cic:/matita/nat/orders/le_to_le_to_eq.con
+cic:/matita/nat/orders/le_to_le_pred.con
+cic:/matita/nat/orders/le_pred_to_le.con
+cic:/matita/nat/orders/le_pred_n.con
+cic:/matita/nat/orders/le_n_m_to_lt_m_Sn_to_eq_n_m.con
+cic:/matita/nat/orders/le_n_fn.con
+cic:/matita/nat/orders/le_n_Sn.con
+cic:/matita/nat/orders/le_n_Sm_elim.con
+cic:/matita/nat/orders/le_n_O_to_eq.con
+cic:/matita/nat/orders/le_n_O_elim.con
+cic:/matita/nat/orders/le_inv.con
+cic:/matita/nat/orders/le_ind.con
+cic:/matita/nat/orders/le_S_S_to_le.con
+cic:/matita/nat/orders/le_S_S.con
+cic:/matita/nat/orders/le_O_n.con
+cic:/matita/nat/orders/leS_to_not_zero.con
+cic:/matita/nat/orders/le.ind
+cic:/matita/nat/orders/increasing_to_monotonic.con
+cic:/matita/nat/orders/increasing_to_le2.con
+cic:/matita/nat/orders/increasing_to_le.con
+cic:/matita/nat/orders/increasing.con
+cic:/matita/nat/orders/gt.con
+cic:/matita/nat/orders/ge.con
+cic:/matita/nat/orders/eq_to_not_lt.con
+cic:/matita/nat/orders/decidable_lt.con
+cic:/matita/nat/orders/decidable_le.con
+cic:/matita/nat/orders/antisymmetric_le.con
+cic:/matita/nat/orders/antisym_le.con
+cic:/matita/nat/orders/S_pred.con
+cic:/matita/nat/orders/Not_lt_n_n.con
+cic:/matita/nat/permutation/transpose_transpose.con
+cic:/matita/nat/permutation/transpose_i_j_j_i.con
+cic:/matita/nat/permutation/transpose_i_j_j.con
+cic:/matita/nat/permutation/transpose_i_j_i.con
+cic:/matita/nat/permutation/transpose_i_i.con
+cic:/matita/nat/permutation/transpose.con
+cic:/matita/nat/permutation/permut_transpose_r.con
+cic:/matita/nat/permutation/permut_transpose_l.con
+cic:/matita/nat/permutation/permut_transpose.con
+cic:/matita/nat/permutation/permut_to_eq_map_iter_i.con
+cic:/matita/nat/permutation/permut_to_bijn.con
+cic:/matita/nat/permutation/permut_n_to_le.con
+cic:/matita/nat/permutation/permut_n_to_eq_n.con
+cic:/matita/nat/permutation/permut_invert_permut.con
+cic:/matita/nat/permutation/permut_fg.con
+cic:/matita/nat/permutation/permut_S_to_permut_transpose.con
+cic:/matita/nat/permutation/permut_S_to_permut.con
+cic:/matita/nat/permutation/permut_O_to_eq_O.con
+cic:/matita/nat/permutation/permut.con
+cic:/matita/nat/permutation/map_iter_i.con
+cic:/matita/nat/permutation/invert_permut_f.con
+cic:/matita/nat/permutation/invert_permut.con
+cic:/matita/nat/permutation/injn_Sn_n.con
+cic:/matita/nat/permutation/injn.con
+cic:/matita/nat/permutation/injective_transpose.con
+cic:/matita/nat/permutation/injective_to_injn.con
+cic:/matita/nat/permutation/injective_invert_permut.con
+cic:/matita/nat/permutation/inj_transpose.con
+cic:/matita/nat/permutation/f_invert_permut.con
+cic:/matita/nat/permutation/eq_transpose.con
+cic:/matita/nat/permutation/eq_to_bijn.con
+cic:/matita/nat/permutation/eq_map_iter_i_transpose_l.con
+cic:/matita/nat/permutation/eq_map_iter_i_transpose_i_Si.con
+cic:/matita/nat/permutation/eq_map_iter_i_transpose2.con
+cic:/matita/nat/permutation/eq_map_iter_i_transpose1.con
+cic:/matita/nat/permutation/eq_map_iter_i_transpose.con
+cic:/matita/nat/permutation/eq_map_iter_i_sigma.con
+cic:/matita/nat/permutation/eq_map_iter_i_pi.con
+cic:/matita/nat/permutation/eq_map_iter_i_fact.con
+cic:/matita/nat/permutation/eq_map_iter_i.con
+cic:/matita/nat/permutation/bijn_transpose_r.con
+cic:/matita/nat/permutation/bijn_transpose_l.con
+cic:/matita/nat/permutation/bijn_transpose.con
+cic:/matita/nat/permutation/bijn_n_Sn.con
+cic:/matita/nat/permutation/bijn_fg.con
+cic:/matita/nat/permutation/bijn_Sn_n.con
+cic:/matita/nat/permutation/bijn.con
+cic:/matita/nat/pi_p/true_to_pi_p_Sn.con
+cic:/matita/nat/pi_p/times_pi_p.con
+cic:/matita/nat/pi_p/pi_p_times.con
+cic:/matita/nat/pi_p/pi_p_pi_p1.con
+cic:/matita/nat/pi_p/pi_p_pi_p.con
+cic:/matita/nat/pi_p/pi_p_knm.con
+cic:/matita/nat/pi_p/pi_p_gi.con
+cic:/matita/nat/pi_p/pi_p_false.con
+cic:/matita/nat/pi_p/pi_p_SO.con
+cic:/matita/nat/pi_p/pi_p2.con
+cic:/matita/nat/pi_p/pi_p2'.con
+cic:/matita/nat/pi_p/pi_p.con
+cic:/matita/nat/pi_p/or_false_eq_SO_to_eq_pi_p.con
+cic:/matita/nat/pi_p/le_pi_p.con
+cic:/matita/nat/pi_p/false_to_pi_p_Sn.con
+cic:/matita/nat/pi_p/false_to_eq_pi_p.con
+cic:/matita/nat/pi_p/exp_times_pi_p.con
+cic:/matita/nat/pi_p/exp_sigma_p1.con
+cic:/matita/nat/pi_p/exp_sigma_p.con
+cic:/matita/nat/pi_p/exp_pi_p.con
+cic:/matita/nat/pi_p/eq_pi_p_gh.con
+cic:/matita/nat/pi_p/eq_pi_p1.con
+cic:/matita/nat/pi_p/eq_pi_p.con
+cic:/matita/nat/plus/sym_plus.con
+cic:/matita/nat/plus/plus_n_Sm.con
+cic:/matita/nat/plus/plus_n_SO.con
+cic:/matita/nat/plus/plus_n_O.con
+cic:/matita/nat/plus/plus.con
+cic:/matita/nat/plus/injective_plus_r.con
+cic:/matita/nat/plus/injective_plus_l.con
+cic:/matita/nat/plus/inj_plus_r.con
+cic:/matita/nat/plus/inj_plus_l.con
+cic:/matita/nat/plus/associative_plus.con
+cic:/matita/nat/plus/assoc_plus.con
+cic:/matita/nat/primes/transitive_divides.con
+cic:/matita/nat/primes/trans_divides.con
+cic:/matita/nat/primes/smallest_factor.con
+cic:/matita/nat/primes/reflexive_divides.con
+cic:/matita/nat/primes/primeb_true_to_prime.con
+cic:/matita/nat/primes/primeb_to_Prop.con
+cic:/matita/nat/primes/primeb_false_to_not_prime.con
+cic:/matita/nat/primes/primeb.con
+cic:/matita/nat/primes/prime_to_smallest_factor.con
+cic:/matita/nat/primes/prime_to_primeb_true.con
+cic:/matita/nat/primes/prime_to_lt_SO.con
+cic:/matita/nat/primes/prime_to_lt_O.con
+cic:/matita/nat/primes/prime_smallest_factor_n.con
+cic:/matita/nat/primes/prime.con
+cic:/matita/nat/primes/or_div_mod1.con
+cic:/matita/nat/primes/not_prime_to_primeb_false.con
+cic:/matita/nat/primes/not_prime_SO.con
+cic:/matita/nat/primes/not_prime_O.con
+cic:/matita/nat/primes/not_divides_to_divides_b_false.con
+cic:/matita/nat/primes/not_divides_S_fact.con
+cic:/matita/nat/primes/mod_S_fact.con
+cic:/matita/nat/primes/mod_O_to_divides.con
+cic:/matita/nat/primes/lt_smallest_factor_to_not_divides.con
+cic:/matita/nat/primes/lt_SO_smallest_factor.con
+cic:/matita/nat/primes/lt_O_smallest_factor.con
+cic:/matita/nat/primes/le_smallest_factor_n.con
+cic:/matita/nat/primes/eq_mod_to_divides.con
+cic:/matita/nat/primes/eq_div_plus.con
+cic:/matita/nat/primes/divides_to_mod_O.con
+cic:/matita/nat/primes/divides_to_lt_O.con
+cic:/matita/nat/primes/divides_to_le.con
+cic:/matita/nat/primes/divides_to_eq_times_div_div_times.con
+cic:/matita/nat/primes/divides_to_divides_b_true1.con
+cic:/matita/nat/primes/divides_to_divides_b_true.con
+cic:/matita/nat/primes/divides_to_div_mod_spec.con
+cic:/matita/nat/primes/divides_to_div.con
+cic:/matita/nat/primes/divides_times.con
+cic:/matita/nat/primes/divides_smallest_factor_n.con
+cic:/matita/nat/primes/divides_plus.con
+cic:/matita/nat/primes/divides_n_n.con
+cic:/matita/nat/primes/divides_n_O.con
+cic:/matita/nat/primes/divides_minus.con
+cic:/matita/nat/primes/divides_ind.con
+cic:/matita/nat/primes/divides_fact.con
+cic:/matita/nat/primes/divides_f_pi_f.con
+cic:/matita/nat/primes/divides_div.con
+cic:/matita/nat/primes/divides_b_true_to_lt_O.con
+cic:/matita/nat/primes/divides_b_true_to_divides1.con
+cic:/matita/nat/primes/divides_b_true_to_divides.con
+cic:/matita/nat/primes/divides_b_to_Prop.con
+cic:/matita/nat/primes/divides_b_false_to_not_divides1.con
+cic:/matita/nat/primes/divides_b_false_to_not_divides.con
+cic:/matita/nat/primes/divides_b_div_true.con
+cic:/matita/nat/primes/divides_b.con
+cic:/matita/nat/primes/divides_SO_n.con
+cic:/matita/nat/primes/divides.ind
+cic:/matita/nat/primes/div_mod_spec_to_divides.con
+cic:/matita/nat/primes/div_div.con
+cic:/matita/nat/primes/decidable_prime.con
+cic:/matita/nat/primes/decidable_divides.con
+cic:/matita/nat/primes/antisymmetric_divides.con
+cic:/matita/nat/relevant_equations/times_plus_plus.con
+cic:/matita/nat/relevant_equations/times_plus_l.con
+cic:/matita/nat/relevant_equations/times_minus_l.con
+cic:/matita/nat/relevant_equations/eq_pred_to_eq.con
+cic:/matita/nat/sigma_and_pi/sigma.con
+cic:/matita/nat/sigma_and_pi/pi.con
+cic:/matita/nat/sigma_and_pi/exp_pi_l.con
+cic:/matita/nat/sigma_and_pi/eq_sigma.con
+cic:/matita/nat/sigma_and_pi/eq_pi.con
+cic:/matita/nat/sigma_and_pi/eq_fact_pi.con
+cic:/matita/nat/sqrt/sqrt.con
+cic:/matita/nat/sqrt/monotonic_sqrt.con
+cic:/matita/nat/sqrt/lt_sqrt_to_le_times_l.con
+cic:/matita/nat/sqrt/lt_sqrt_n.con
+cic:/matita/nat/sqrt/lt_sqrt.con
+cic:/matita/nat/sqrt/leq_sqrt_n.con
+cic:/matita/nat/sqrt/le_sqrt_to_le_times_r.con
+cic:/matita/nat/sqrt/le_sqrt_to_le_times_l.con
+cic:/matita/nat/sqrt/le_sqrt_nl.con
+cic:/matita/nat/sqrt/le_sqrt_n_n.con
+cic:/matita/nat/sqrt/le_sqrt_n1.con
+cic:/matita/nat/sqrt/le_sqrt_log_n.con
+cic:/matita/nat/sqrt/eq_sqrt.con
+cic:/matita/nat/times/times_n_Sm.con
+cic:/matita/nat/times/times_n_SO.con
+cic:/matita/nat/times/times_n_O.con
+cic:/matita/nat/times/times_SSO_n.con
+cic:/matita/nat/times/times_SSO.con
+cic:/matita/nat/times/times_O_to_O.con
+cic:/matita/nat/times/times.con
+cic:/matita/nat/times/symmetric_times.con
+cic:/matita/nat/times/sym_times.con
+cic:/matita/nat/times/or_eq_eq_S.con
+cic:/matita/nat/times/distributive_times_plus.con
+cic:/matita/nat/times/distr_times_plus.con
+cic:/matita/nat/times/associative_times.con
+cic:/matita/nat/times/assoc_times.con
+cic:/matita/nat/totient/totient_times.con
+cic:/matita/nat/totient/totient.con
+cic:/matita/nat/totient1/sigma_p_Sn_divides_b_totient_n.con
+cic:/matita/nat/totient1/lt_O_to_divides_to_lt_O_div.con
cic:/matita/technicalities/setoids/variance_rect.con
cic:/matita/technicalities/setoids/variance_rec.con
cic:/matita/technicalities/setoids/variance_of_argument_class.con
cic:/matita/technicalities/setoids/rewrite_direction_ind.con
cic:/matita/technicalities/setoids/rewrite_direction.ind
cic:/matita/technicalities/setoids/relation_of_relation_class.con
+cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con
cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con
cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con
cic:/matita/technicalities/setoids/relation_class_of_argument_class.con
cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con
-cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con
cic:/matita/technicalities/setoids/product_of_arguments.con
cic:/matita/technicalities/setoids/opposite_direction_idempotent.con
cic:/matita/technicalities/setoids/opposite_direction.con
cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con
cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con
cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind
-# # mutual fix
-# cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
-# # depending on the previous
-# cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con
-# cic:/matita/demo/propositional_sequent_calculus/elim_not.con
-# cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con
-# cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con
-# cic:/matita/demo/propositional_sequent_calculus/derive_inv.con
-# cic:/matita/demo/propositional_sequent_calculus/derive_ind.con
-# cic:/matita/demo/propositional_sequent_calculus/derive.ind
-# cic:/matita/demo/propositional_sequent_calculus/demorgan2.con
-# cic:/matita/demo/propositional_sequent_calculus/demorgan1.con
-# cic:/matita/demo/propositional_sequent_calculus/daemon.con
-# cic:/matita/demo/propositional_sequent_calculus/completeness_base.con
-# cic:/matita/demo/propositional_sequent_calculus/associative_andb.con
-# cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con
-# cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con
-# cic:/matita/demo/propositional_sequent_calculus/and_of_list.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula.ind
projects / helm.git / commitdiff