cic:/Coq/Arith/Between/P_nth_ind.con
cic:/Coq/Arith/Between/bet_eq.con
cic:/Coq/Arith/Between/between_Sk_l.con
cic:/Coq/Arith/Between/between_in_int.con
cic:/Coq/Arith/Between/between_ind.con
cic:/Coq/Arith/Between/between_le.con
cic:/Coq/Arith/Between/between_not_exists.con
cic:/Coq/Arith/Between/between_or_exists.con
cic:/Coq/Arith/Between/between_restr.con
cic:/Coq/Arith/Between/event_O.con
cic:/Coq/Arith/Between/eventually.con
cic:/Coq/Arith/Between/exists_S_le.con
cic:/Coq/Arith/Between/exists_between_ind.con
cic:/Coq/Arith/Between/exists_in_int.con
cic:/Coq/Arith/Between/exists_le_S.con
cic:/Coq/Arith/Between/exists_lt.con
cic:/Coq/Arith/Between/in_int.con
cic:/Coq/Arith/Between/in_int_S.con
cic:/Coq/Arith/Between/in_int_Sp_q.con
cic:/Coq/Arith/Between/in_int_between.con
cic:/Coq/Arith/Between/in_int_exists.con
cic:/Coq/Arith/Between/in_int_intro.con
cic:/Coq/Arith/Between/in_int_lt.con
cic:/Coq/Arith/Between/in_int_p_Sq.con
cic:/Coq/Arith/Between/nth_le.con
cic:/Coq/Arith/Bool_nat/lt_ge_dec.con
cic:/Coq/Arith/Bool_nat/nat_eq_bool.con
cic:/Coq/Arith/Bool_nat/nat_ge_lt_bool.con
cic:/Coq/Arith/Bool_nat/nat_gt_le_bool.con
cic:/Coq/Arith/Bool_nat/nat_le_gt_bool.con
cic:/Coq/Arith/Bool_nat/nat_lt_ge_bool.con
cic:/Coq/Arith/Bool_nat/nat_noteq_bool.con
cic:/Coq/Arith/Bool_nat/notzerop.con
cic:/Coq/Arith/Bool_nat/notzerop_bool.con
cic:/Coq/Arith/Bool_nat/zerop_bool.con
cic:/Coq/Arith/Compare/Pcompare.con
cic:/Coq/Arith/Compare/discrete_nat.con
cic:/Coq/Arith/Compare/le_dec.con
cic:/Coq/Arith/Compare/le_decide.con
cic:/Coq/Arith/Compare/le_le_S_eq.con
cic:/Coq/Arith/Compare/le_or_le_S.con
cic:/Coq/Arith/Compare/lt_or_eq.con
cic:/Coq/Arith/Compare_dec/dec_ge.con
cic:/Coq/Arith/Compare_dec/dec_gt.con
cic:/Coq/Arith/Compare_dec/dec_le.con
cic:/Coq/Arith/Compare_dec/dec_lt.con
cic:/Coq/Arith/Compare_dec/gt_eq_gt_dec.con
cic:/Coq/Arith/Compare_dec/le_ge_dec.con
cic:/Coq/Arith/Compare_dec/le_gt_dec.con
cic:/Coq/Arith/Compare_dec/le_le_S_dec.con
cic:/Coq/Arith/Compare_dec/le_lt_dec.con
cic:/Coq/Arith/Compare_dec/le_lt_eq_dec.con
cic:/Coq/Arith/Compare_dec/lt_eq_lt_dec.con
cic:/Coq/Arith/Compare_dec/not_eq.con
cic:/Coq/Arith/Compare_dec/not_ge.con
cic:/Coq/Arith/Compare_dec/not_gt.con
cic:/Coq/Arith/Compare_dec/not_le.con
cic:/Coq/Arith/Compare_dec/not_lt.con
cic:/Coq/Arith/Compare_dec/zerop.con
cic:/Coq/Arith/Div2/div2.con
cic:/Coq/Arith/Div2/div2_even.con
cic:/Coq/Arith/Div2/div2_odd.con
cic:/Coq/Arith/Div2/double.con
cic:/Coq/Arith/Div2/double_S.con
cic:/Coq/Arith/Div2/double_even.con
cic:/Coq/Arith/Div2/double_odd.con
cic:/Coq/Arith/Div2/double_plus.con
cic:/Coq/Arith/Div2/even_2n.con
cic:/Coq/Arith/Div2/even_div2.con
cic:/Coq/Arith/Div2/even_double.con
cic:/Coq/Arith/Div2/even_odd_div2.con
cic:/Coq/Arith/Div2/even_odd_double.con
cic:/Coq/Arith/Div2/ind_0_1_SS.con
cic:/Coq/Arith/Div2/lt_div2.con
cic:/Coq/Arith/Div2/odd_S2n.con
cic:/Coq/Arith/Div2/odd_div2.con
cic:/Coq/Arith/Div2/odd_double.con
cic:/Coq/Arith/EqNat/beq_nat.con
cic:/Coq/Arith/EqNat/beq_nat_eq.con
cic:/Coq/Arith/EqNat/beq_nat_refl.con
cic:/Coq/Arith/EqNat/eq_eq_nat.con
cic:/Coq/Arith/EqNat/eq_nat.con
cic:/Coq/Arith/EqNat/eq_nat_decide.con
cic:/Coq/Arith/EqNat/eq_nat_elim.con
cic:/Coq/Arith/EqNat/eq_nat_eq.con
cic:/Coq/Arith/EqNat/eq_nat_refl.con
cic:/Coq/Arith/Euclid/diveucl_ind.con
cic:/Coq/Arith/Euclid/diveucl_rec.con
cic:/Coq/Arith/Euclid/diveucl_rect.con
cic:/Coq/Arith/Euclid/eucl_dev.con
cic:/Coq/Arith/Euclid/modulo.con
cic:/Coq/Arith/Euclid/quotient.con
cic:/Coq/Arith/Even/even_even_plus.con
cic:/Coq/Arith/Even/even_ind.con
cic:/Coq/Arith/Even/even_mult_aux.con
cic:/Coq/Arith/Even/even_mult_inv_l.con
cic:/Coq/Arith/Even/even_mult_inv_r.con
cic:/Coq/Arith/Even/even_mult_l.con
cic:/Coq/Arith/Even/even_mult_r.con
cic:/Coq/Arith/Even/even_odd_dec.con
cic:/Coq/Arith/Even/even_or_odd.con
cic:/Coq/Arith/Even/even_plus_aux.con
cic:/Coq/Arith/Even/even_plus_even_inv_l.con
cic:/Coq/Arith/Even/even_plus_even_inv_r.con
cic:/Coq/Arith/Even/even_plus_odd_inv_l.con
cic:/Coq/Arith/Even/even_plus_odd_inv_r.con
cic:/Coq/Arith/Even/not_even_and_odd.con
cic:/Coq/Arith/Even/odd_even_plus.con
cic:/Coq/Arith/Even/odd_ind.con
cic:/Coq/Arith/Even/odd_mult.con
cic:/Coq/Arith/Even/odd_mult_inv_l.con
cic:/Coq/Arith/Even/odd_mult_inv_r.con
cic:/Coq/Arith/Even/odd_plus_even_inv_l.con
cic:/Coq/Arith/Even/odd_plus_even_inv_r.con
cic:/Coq/Arith/Even/odd_plus_l.con
cic:/Coq/Arith/Even/odd_plus_odd_inv_l.con
cic:/Coq/Arith/Even/odd_plus_odd_inv_r.con
cic:/Coq/Arith/Even/odd_plus_r.con
cic:/Coq/Arith/Factorial/fact.con
cic:/Coq/Arith/Factorial/fact_le.con
cic:/Coq/Arith/Factorial/fact_neq_0.con
cic:/Coq/Arith/Factorial/lt_O_fact.con
cic:/Coq/Arith/Gt/gt_O_eq.con
cic:/Coq/Arith/Gt/gt_S.con
cic:/Coq/Arith/Gt/gt_S_le.con
cic:/Coq/Arith/Gt/gt_S_n.con
cic:/Coq/Arith/Gt/gt_Sn_O.con
cic:/Coq/Arith/Gt/gt_Sn_n.con
cic:/Coq/Arith/Gt/gt_asym.con
cic:/Coq/Arith/Gt/gt_irrefl.con
cic:/Coq/Arith/Gt/gt_le_S.con
cic:/Coq/Arith/Gt/gt_le_trans.con
cic:/Coq/Arith/Gt/gt_n_S.con
cic:/Coq/Arith/Gt/gt_not_le.con
cic:/Coq/Arith/Gt/gt_pred.con
cic:/Coq/Arith/Gt/gt_trans.con
cic:/Coq/Arith/Gt/gt_trans_S.con
cic:/Coq/Arith/Gt/le_S_gt.con
cic:/Coq/Arith/Gt/le_gt_S.con
cic:/Coq/Arith/Gt/le_gt_trans.con
cic:/Coq/Arith/Gt/le_not_gt.con
cic:/Coq/Arith/Gt/plus_gt_compat_l.con
cic:/Coq/Arith/Gt/plus_gt_reg_l.con
cic:/Coq/Arith/Le/le_O_n.con
cic:/Coq/Arith/Le/le_S_n.con
cic:/Coq/Arith/Le/le_Sn_O.con
cic:/Coq/Arith/Le/le_Sn_le.con
cic:/Coq/Arith/Le/le_Sn_n.con
cic:/Coq/Arith/Le/le_antisym.con
cic:/Coq/Arith/Le/le_elim_rel.con
cic:/Coq/Arith/Le/le_n_O_eq.con
cic:/Coq/Arith/Le/le_n_S.con
cic:/Coq/Arith/Le/le_n_Sn.con
cic:/Coq/Arith/Le/le_pred.con
cic:/Coq/Arith/Le/le_pred_n.con
cic:/Coq/Arith/Le/le_refl.con
cic:/Coq/Arith/Le/le_trans.con
cic:/Coq/Arith/Lt/S_pred.con
cic:/Coq/Arith/Lt/le_lt_n_Sm.con
cic:/Coq/Arith/Lt/le_lt_or_eq.con
cic:/Coq/Arith/Lt/le_lt_trans.con
cic:/Coq/Arith/Lt/le_not_lt.con
cic:/Coq/Arith/Lt/le_or_lt.con
cic:/Coq/Arith/Lt/lt_O_Sn.con
cic:/Coq/Arith/Lt/lt_O_neq.con
cic:/Coq/Arith/Lt/lt_S.con
cic:/Coq/Arith/Lt/lt_S_n.con
cic:/Coq/Arith/Lt/lt_asym.con
cic:/Coq/Arith/Lt/lt_irrefl.con
cic:/Coq/Arith/Lt/lt_le_S.con
cic:/Coq/Arith/Lt/lt_le_trans.con
cic:/Coq/Arith/Lt/lt_le_weak.con
cic:/Coq/Arith/Lt/lt_n_O.con
cic:/Coq/Arith/Lt/lt_n_S.con
cic:/Coq/Arith/Lt/lt_n_Sm_le.con
cic:/Coq/Arith/Lt/lt_n_Sn.con
cic:/Coq/Arith/Lt/lt_not_le.con
cic:/Coq/Arith/Lt/lt_pred.con
cic:/Coq/Arith/Lt/lt_pred_n_n.con
cic:/Coq/Arith/Lt/lt_trans.con
cic:/Coq/Arith/Lt/nat_total_order.con
cic:/Coq/Arith/Lt/neq_O_lt.con
cic:/Coq/Arith/Max/le_max_l.con
cic:/Coq/Arith/Max/le_max_r.con
cic:/Coq/Arith/Max/max.con
cic:/Coq/Arith/Max/max_SS.con
cic:/Coq/Arith/Max/max_case.con
cic:/Coq/Arith/Max/max_case2.con
cic:/Coq/Arith/Max/max_comm.con
cic:/Coq/Arith/Max/max_dec.con
cic:/Coq/Arith/Max/max_l.con
cic:/Coq/Arith/Max/max_r.con
cic:/Coq/Arith/Min/le_min_l.con
cic:/Coq/Arith/Min/le_min_r.con
cic:/Coq/Arith/Min/min.con
cic:/Coq/Arith/Min/min_SS.con
cic:/Coq/Arith/Min/min_case.con
cic:/Coq/Arith/Min/min_case2.con
cic:/Coq/Arith/Min/min_comm.con
cic:/Coq/Arith/Min/min_dec.con
cic:/Coq/Arith/Min/min_l.con
cic:/Coq/Arith/Min/min_r.con
cic:/Coq/Arith/Minus/le_minus.con
cic:/Coq/Arith/Minus/le_plus_minus.con
cic:/Coq/Arith/Minus/le_plus_minus_r.con
cic:/Coq/Arith/Minus/lt_O_minus_lt.con
cic:/Coq/Arith/Minus/lt_minus.con
cic:/Coq/Arith/Minus/minus_Sn_m.con
cic:/Coq/Arith/Minus/minus_n_O.con
cic:/Coq/Arith/Minus/minus_n_n.con
cic:/Coq/Arith/Minus/minus_plus.con
cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con
cic:/Coq/Arith/Minus/not_le_minus_0.con
cic:/Coq/Arith/Minus/plus_minus.con
cic:/Coq/Arith/Minus/pred_of_minus.con
cic:/Coq/Arith/Mult/mult_0_l.con
cic:/Coq/Arith/Mult/mult_0_r.con
cic:/Coq/Arith/Mult/mult_1_l.con
cic:/Coq/Arith/Mult/mult_1_r.con
cic:/Coq/Arith/Mult/mult_O_le.con
cic:/Coq/Arith/Mult/mult_S_le_reg_l.con
cic:/Coq/Arith/Mult/mult_S_lt_compat_l.con
cic:/Coq/Arith/Mult/mult_acc.con
cic:/Coq/Arith/Mult/mult_acc_aux.con
cic:/Coq/Arith/Mult/mult_assoc.con
cic:/Coq/Arith/Mult/mult_assoc_reverse.con
cic:/Coq/Arith/Mult/mult_comm.con
cic:/Coq/Arith/Mult/mult_le_compat.con
cic:/Coq/Arith/Mult/mult_le_compat_l.con
cic:/Coq/Arith/Mult/mult_le_compat_r.con
cic:/Coq/Arith/Mult/mult_lt_compat_r.con
cic:/Coq/Arith/Mult/mult_minus_distr_r.con
cic:/Coq/Arith/Mult/mult_plus_distr_l.con
cic:/Coq/Arith/Mult/mult_plus_distr_r.con
cic:/Coq/Arith/Mult/mult_tail_mult.con
cic:/Coq/Arith/Mult/odd_even_lem.con
cic:/Coq/Arith/Mult/tail_mult.con
cic:/Coq/Arith/Peano_dec/O_or_S.con
cic:/Coq/Arith/Peano_dec/dec_eq_nat.con
cic:/Coq/Arith/Peano_dec/eq_nat_dec.con
cic:/Coq/Arith/Plus/le_plus_l.con
cic:/Coq/Arith/Plus/le_plus_r.con
cic:/Coq/Arith/Plus/le_plus_trans.con
cic:/Coq/Arith/Plus/lt_plus_trans.con
cic:/Coq/Arith/Plus/plus_0_l.con
cic:/Coq/Arith/Plus/plus_0_r.con
cic:/Coq/Arith/Plus/plus_Snm_nSm.con
cic:/Coq/Arith/Plus/plus_acc.con
cic:/Coq/Arith/Plus/plus_assoc.con
cic:/Coq/Arith/Plus/plus_assoc_reverse.con
cic:/Coq/Arith/Plus/plus_comm.con
cic:/Coq/Arith/Plus/plus_is_O.con
cic:/Coq/Arith/Plus/plus_is_one.con
cic:/Coq/Arith/Plus/plus_le_compat.con
cic:/Coq/Arith/Plus/plus_le_compat_l.con
cic:/Coq/Arith/Plus/plus_le_compat_r.con
cic:/Coq/Arith/Plus/plus_le_lt_compat.con
cic:/Coq/Arith/Plus/plus_le_reg_l.con
cic:/Coq/Arith/Plus/plus_lt_compat.con
cic:/Coq/Arith/Plus/plus_lt_compat_l.con
cic:/Coq/Arith/Plus/plus_lt_compat_r.con
cic:/Coq/Arith/Plus/plus_lt_le_compat.con
cic:/Coq/Arith/Plus/plus_lt_reg_l.con
cic:/Coq/Arith/Plus/plus_permute.con
cic:/Coq/Arith/Plus/plus_permute_2_in_4.con
cic:/Coq/Arith/Plus/plus_reg_l.con
cic:/Coq/Arith/Plus/plus_tail_plus.con
cic:/Coq/Arith/Plus/tail_plus.con
cic:/Coq/Arith/Wf_nat/acc_lt_rel.con
cic:/Coq/Arith/Wf_nat/gt_wf_ind.con
cic:/Coq/Arith/Wf_nat/gt_wf_rec.con
cic:/Coq/Arith/Wf_nat/gtof.con
cic:/Coq/Arith/Wf_nat/induction_gtof1.con
cic:/Coq/Arith/Wf_nat/induction_gtof2.con
cic:/Coq/Arith/Wf_nat/induction_ltof1.con
cic:/Coq/Arith/Wf_nat/induction_ltof2.con
cic:/Coq/Arith/Wf_nat/inv_lt_rel.con
cic:/Coq/Arith/Wf_nat/lt_wf.con
cic:/Coq/Arith/Wf_nat/lt_wf_double_ind.con
cic:/Coq/Arith/Wf_nat/lt_wf_double_rec.con
cic:/Coq/Arith/Wf_nat/lt_wf_ind.con
cic:/Coq/Arith/Wf_nat/lt_wf_rec.con
cic:/Coq/Arith/Wf_nat/lt_wf_rec1.con
cic:/Coq/Arith/Wf_nat/ltof.con
cic:/Coq/Arith/Wf_nat/well_founded_gtof.con
cic:/Coq/Arith/Wf_nat/well_founded_inv_lt_rel_compat.con
cic:/Coq/Arith/Wf_nat/well_founded_inv_rel_inv_lt_rel.con
cic:/Coq/Arith/Wf_nat/well_founded_lt_compat.con
cic:/Coq/Arith/Wf_nat/well_founded_ltof.con
cic:/Coq/Bool/Bool/Is_true.con
cic:/Coq/Bool/Bool/Is_true_eq_left.con
cic:/Coq/Bool/Bool/Is_true_eq_right.con
cic:/Coq/Bool/Bool/Is_true_eq_true.con
cic:/Coq/Bool/Bool/Is_true_eq_true2.con
cic:/Coq/Bool/Bool/absoption_andb.con
cic:/Coq/Bool/Bool/absoption_orb.con
cic:/Coq/Bool/Bool/andb.con
cic:/Coq/Bool/Bool/andb_assoc.con
cic:/Coq/Bool/Bool/andb_b_false.con
cic:/Coq/Bool/Bool/andb_b_true.con
cic:/Coq/Bool/Bool/andb_comm.con
cic:/Coq/Bool/Bool/andb_false_b.con
cic:/Coq/Bool/Bool/andb_false_elim.con
cic:/Coq/Bool/Bool/andb_false_intro1.con
cic:/Coq/Bool/Bool/andb_false_intro2.con
cic:/Coq/Bool/Bool/andb_neg_b.con
cic:/Coq/Bool/Bool/andb_prop.con
cic:/Coq/Bool/Bool/andb_prop2.con
cic:/Coq/Bool/Bool/andb_true_b.con
cic:/Coq/Bool/Bool/andb_true_eq.con
cic:/Coq/Bool/Bool/andb_true_intro.con
cic:/Coq/Bool/Bool/andb_true_intro2.con
cic:/Coq/Bool/Bool/bool_1.con
cic:/Coq/Bool/Bool/bool_2.con
cic:/Coq/Bool/Bool/bool_3.con
cic:/Coq/Bool/Bool/bool_4.con
cic:/Coq/Bool/Bool/bool_5.con
cic:/Coq/Bool/Bool/bool_6.con
cic:/Coq/Bool/Bool/demorgan1.con
cic:/Coq/Bool/Bool/demorgan2.con
cic:/Coq/Bool/Bool/demorgan3.con
cic:/Coq/Bool/Bool/demorgan4.con
cic:/Coq/Bool/Bool/diff_false_true.con
cic:/Coq/Bool/Bool/diff_true_false.con
cic:/Coq/Bool/Bool/eq_true_false_abs.con
cic:/Coq/Bool/Bool/eqb.con
cic:/Coq/Bool/Bool/eqb_eq.con
cic:/Coq/Bool/Bool/eqb_negb1.con
cic:/Coq/Bool/Bool/eqb_negb2.con
cic:/Coq/Bool/Bool/eqb_prop.con
cic:/Coq/Bool/Bool/eqb_refl.con
cic:/Coq/Bool/Bool/eqb_reflx.con
cic:/Coq/Bool/Bool/eqb_subst.con
cic:/Coq/Bool/Bool/false_xorb.con
cic:/Coq/Bool/Bool/if_negb.con
cic:/Coq/Bool/Bool/ifb.con
cic:/Coq/Bool/Bool/implb.con
cic:/Coq/Bool/Bool/leb.con
cic:/Coq/Bool/Bool/negb.con
cic:/Coq/Bool/Bool/negb_andb.con
cic:/Coq/Bool/Bool/negb_elim.con
cic:/Coq/Bool/Bool/negb_intro.con
cic:/Coq/Bool/Bool/negb_orb.con
cic:/Coq/Bool/Bool/negb_sym.con
cic:/Coq/Bool/Bool/no_fixpoint_negb.con
cic:/Coq/Bool/Bool/not_false_is_true.con
cic:/Coq/Bool/Bool/not_true_is_false.con
cic:/Coq/Bool/Bool/orb.con
cic:/Coq/Bool/Bool/orb_assoc.con
cic:/Coq/Bool/Bool/orb_b_false.con
cic:/Coq/Bool/Bool/orb_b_true.con
cic:/Coq/Bool/Bool/orb_comm.con
cic:/Coq/Bool/Bool/orb_false_b.con
cic:/Coq/Bool/Bool/orb_false_elim.con
cic:/Coq/Bool/Bool/orb_false_intro.con
cic:/Coq/Bool/Bool/orb_neg_b.con
cic:/Coq/Bool/Bool/orb_prop.con
cic:/Coq/Bool/Bool/orb_prop2.con
cic:/Coq/Bool/Bool/orb_true_b.con
cic:/Coq/Bool/Bool/orb_true_elim.con
cic:/Coq/Bool/Bool/orb_true_intro.con
cic:/Coq/Bool/Bool/true_xorb.con
cic:/Coq/Bool/Bool/xorb.con
cic:/Coq/Bool/Bool/xorb_assoc.con
cic:/Coq/Bool/Bool/xorb_comm.con
cic:/Coq/Bool/Bool/xorb_eq.con
cic:/Coq/Bool/Bool/xorb_false.con
cic:/Coq/Bool/Bool/xorb_move_l_r_1.con
cic:/Coq/Bool/Bool/xorb_move_l_r_2.con
cic:/Coq/Bool/Bool/xorb_move_r_l_1.con
cic:/Coq/Bool/Bool/xorb_move_r_l_2.con
cic:/Coq/Bool/Bool/xorb_nilpotent.con
cic:/Coq/Bool/Bool/xorb_true.con
cic:/Coq/Bool/BoolEq/beq_eq_not_false.con
cic:/Coq/Bool/BoolEq/beq_eq_true.con
cic:/Coq/Bool/BoolEq/beq_false_not_eq.con
cic:/Coq/Bool/BoolEq/eq_dec.con
cic:/Coq/Bool/BoolEq/exists_beq_eq.con
cic:/Coq/Bool/BoolEq/not_eq_false_beq.con
cic:/Coq/Bool/Bvector/BVand.con
cic:/Coq/Bool/Bvector/BVor.con
cic:/Coq/Bool/Bvector/BVxor.con
cic:/Coq/Bool/Bvector/Bcons.con
cic:/Coq/Bool/Bvector/Bhigh.con
cic:/Coq/Bool/Bvector/Blow.con
cic:/Coq/Bool/Bvector/Bneg.con
cic:/Coq/Bool/Bvector/Bnil.con
cic:/Coq/Bool/Bvector/BshiftL.con
cic:/Coq/Bool/Bvector/BshiftL_iter.con
cic:/Coq/Bool/Bvector/BshiftRa.con
cic:/Coq/Bool/Bvector/BshiftRa_iter.con
cic:/Coq/Bool/Bvector/BshiftRl.con
cic:/Coq/Bool/Bvector/BshiftRl_iter.con
cic:/Coq/Bool/Bvector/Bsign.con
cic:/Coq/Bool/Bvector/Bvect_false.con
cic:/Coq/Bool/Bvector/Bvect_true.con
cic:/Coq/Bool/Bvector/Bvector.con
cic:/Coq/Bool/Bvector/Vbinary.con
cic:/Coq/Bool/Bvector/Vconst.con
cic:/Coq/Bool/Bvector/Vextend.con
cic:/Coq/Bool/Bvector/Vhead.con
cic:/Coq/Bool/Bvector/Vlast.con
cic:/Coq/Bool/Bvector/Vshiftin.con
cic:/Coq/Bool/Bvector/Vshiftout.con
cic:/Coq/Bool/Bvector/Vshiftrepeat.con
cic:/Coq/Bool/Bvector/Vtail.con
cic:/Coq/Bool/Bvector/Vtrunc.con
cic:/Coq/Bool/Bvector/Vunary.con
cic:/Coq/Bool/Bvector/vector_ind.con
cic:/Coq/Bool/Bvector/vector_rec.con
cic:/Coq/Bool/Bvector/vector_rect.con
cic:/Coq/Bool/DecBool/ifdec.con
cic:/Coq/Bool/DecBool/ifdec_left.con
cic:/Coq/Bool/DecBool/ifdec_right.con
cic:/Coq/Bool/IfProp/IfProp_false.con
cic:/Coq/Bool/IfProp/IfProp_ind.con
cic:/Coq/Bool/IfProp/IfProp_or.con
cic:/Coq/Bool/IfProp/IfProp_sum.con
cic:/Coq/Bool/IfProp/IfProp_true.con
cic:/Coq/Bool/IfProp/Iffalse_inv.con
cic:/Coq/Bool/IfProp/Iftrue_inv.con
cic:/Coq/Bool/Sumbool/bool_eq_ind.con
cic:/Coq/Bool/Sumbool/bool_eq_rec.con
cic:/Coq/Bool/Sumbool/bool_of_sumbool.con
cic:/Coq/Bool/Sumbool/sumbool_and.con
cic:/Coq/Bool/Sumbool/sumbool_not.con
cic:/Coq/Bool/Sumbool/sumbool_of_bool.con
cic:/Coq/Bool/Sumbool/sumbool_or.con
cic:/Coq/Bool/Zerob/zerob.con
cic:/Coq/Bool/Zerob/zerob_false_elim.con
cic:/Coq/Bool/Zerob/zerob_false_intro.con
cic:/Coq/Bool/Zerob/zerob_true_elim.con
cic:/Coq/Bool/Zerob/zerob_true_intro.con
cic:/Coq/Init/Datatypes/CompOpp.con
cic:/Coq/Init/Datatypes/Empty_set_ind.con
cic:/Coq/Init/Datatypes/Empty_set_rec.con
cic:/Coq/Init/Datatypes/Empty_set_rect.con
cic:/Coq/Init/Datatypes/bool_ind.con
cic:/Coq/Init/Datatypes/bool_rec.con
cic:/Coq/Init/Datatypes/bool_rect.con
cic:/Coq/Init/Datatypes/comparison_ind.con
cic:/Coq/Init/Datatypes/comparison_rec.con
cic:/Coq/Init/Datatypes/comparison_rect.con
cic:/Coq/Init/Datatypes/fst.con
cic:/Coq/Init/Datatypes/identity_ind.con
cic:/Coq/Init/Datatypes/identity_rec.con
cic:/Coq/Init/Datatypes/identity_rect.con
cic:/Coq/Init/Datatypes/injective_projections.con
cic:/Coq/Init/Datatypes/nat_ind.con
cic:/Coq/Init/Datatypes/nat_rec.con
cic:/Coq/Init/Datatypes/nat_rect.con
cic:/Coq/Init/Datatypes/option_ind.con
cic:/Coq/Init/Datatypes/option_rec.con
cic:/Coq/Init/Datatypes/option_rect.con
cic:/Coq/Init/Datatypes/prod_ind.con
cic:/Coq/Init/Datatypes/prod_rec.con
cic:/Coq/Init/Datatypes/prod_rect.con
cic:/Coq/Init/Datatypes/snd.con
cic:/Coq/Init/Datatypes/sum_ind.con
cic:/Coq/Init/Datatypes/sum_rec.con
cic:/Coq/Init/Datatypes/sum_rect.con
cic:/Coq/Init/Datatypes/surjective_pairing.con
cic:/Coq/Init/Datatypes/unit_ind.con
cic:/Coq/Init/Datatypes/unit_rec.con
cic:/Coq/Init/Datatypes/unit_rect.con
cic:/Coq/Init/Logic/False_ind.con
cic:/Coq/Init/Logic/False_rec.con
cic:/Coq/Init/Logic/False_rect.con
cic:/Coq/Init/Logic/IF_then_else.con
cic:/Coq/Init/Logic/True_ind.con
cic:/Coq/Init/Logic/True_rec.con
cic:/Coq/Init/Logic/True_rect.con
cic:/Coq/Init/Logic/absurd.con
cic:/Coq/Init/Logic/all.con
cic:/Coq/Init/Logic/and_ind.con
cic:/Coq/Init/Logic/and_rec.con
cic:/Coq/Init/Logic/and_rect.con
cic:/Coq/Init/Logic/eq_ind.con
cic:/Coq/Init/Logic/eq_ind_r.con
cic:/Coq/Init/Logic/eq_rec.con
cic:/Coq/Init/Logic/eq_rec_r.con
cic:/Coq/Init/Logic/eq_rect.con
cic:/Coq/Init/Logic/eq_rect_r.con
cic:/Coq/Init/Logic/ex2_ind.con
cic:/Coq/Init/Logic/ex_ind.con
cic:/Coq/Init/Logic/f_equal.con
cic:/Coq/Init/Logic/f_equal2.con
cic:/Coq/Init/Logic/f_equal3.con
cic:/Coq/Init/Logic/f_equal4.con
cic:/Coq/Init/Logic/f_equal5.con
cic:/Coq/Init/Logic/gen.con
cic:/Coq/Init/Logic/iff.con
cic:/Coq/Init/Logic/iff_refl.con
cic:/Coq/Init/Logic/iff_sym.con
cic:/Coq/Init/Logic/iff_trans.con
cic:/Coq/Init/Logic/inst.con
cic:/Coq/Init/Logic/not.con
cic:/Coq/Init/Logic/or_ind.con
cic:/Coq/Init/Logic/proj1.con
cic:/Coq/Init/Logic/proj2.con
cic:/Coq/Init/Logic/sym_eq.con
cic:/Coq/Init/Logic/sym_equal.con
cic:/Coq/Init/Logic/sym_not_eq.con
cic:/Coq/Init/Logic/sym_not_equal.con
cic:/Coq/Init/Logic/trans_eq.con
cic:/Coq/Init/Logic/trans_equal.con
cic:/Coq/Init/Logic_Type/congr_id.con
cic:/Coq/Init/Logic_Type/fstT.con
cic:/Coq/Init/Logic_Type/identity_ind_r.con
cic:/Coq/Init/Logic_Type/identity_rec_r.con
cic:/Coq/Init/Logic_Type/identity_rect_r.con
cic:/Coq/Init/Logic_Type/notT.con
cic:/Coq/Init/Logic_Type/prodT_curry.con
cic:/Coq/Init/Logic_Type/prodT_ind.con
cic:/Coq/Init/Logic_Type/prodT_rec.con
cic:/Coq/Init/Logic_Type/prodT_rect.con
cic:/Coq/Init/Logic_Type/prodT_uncurry.con
cic:/Coq/Init/Logic_Type/sndT.con
cic:/Coq/Init/Logic_Type/sym_id.con
cic:/Coq/Init/Logic_Type/sym_not_id.con
cic:/Coq/Init/Logic_Type/trans_id.con
cic:/Coq/Init/Peano/IsSucc.con
cic:/Coq/Init/Peano/O_S.con
cic:/Coq/Init/Peano/eq_S.con
cic:/Coq/Init/Peano/eq_add_S.con
cic:/Coq/Init/Peano/ge.con
cic:/Coq/Init/Peano/gt.con
cic:/Coq/Init/Peano/le_ind.con
cic:/Coq/Init/Peano/lt.con
cic:/Coq/Init/Peano/minus.con
cic:/Coq/Init/Peano/mult.con
cic:/Coq/Init/Peano/mult_n_O.con
cic:/Coq/Init/Peano/mult_n_Sm.con
cic:/Coq/Init/Peano/n_Sn.con
cic:/Coq/Init/Peano/nat_case.con
cic:/Coq/Init/Peano/nat_double_ind.con
cic:/Coq/Init/Peano/not_eq_S.con
cic:/Coq/Init/Peano/plus.con
cic:/Coq/Init/Peano/plus_O_n.con
cic:/Coq/Init/Peano/plus_Sn_m.con
cic:/Coq/Init/Peano/plus_n_O.con
cic:/Coq/Init/Peano/plus_n_Sm.con
cic:/Coq/Init/Peano/pred.con
cic:/Coq/Init/Peano/pred_Sn.con
cic:/Coq/Init/Specif/Choice.con
cic:/Coq/Init/Specif/Choice2.con
cic:/Coq/Init/Specif/Exc.con
cic:/Coq/Init/Specif/absurd_set.con
cic:/Coq/Init/Specif/bool_choice.con
cic:/Coq/Init/Specif/error.con
cic:/Coq/Init/Specif/except.con
cic:/Coq/Init/Specif/proj1_sig.con
cic:/Coq/Init/Specif/proj2_sig.con
cic:/Coq/Init/Specif/projS1.con
cic:/Coq/Init/Specif/projS2.con
cic:/Coq/Init/Specif/projT1.con
cic:/Coq/Init/Specif/projT2.con
cic:/Coq/Init/Specif/sig2_ind.con
cic:/Coq/Init/Specif/sig2_rec.con
cic:/Coq/Init/Specif/sig2_rect.con
cic:/Coq/Init/Specif/sigS2_ind.con
cic:/Coq/Init/Specif/sigS2_rec.con
cic:/Coq/Init/Specif/sigS2_rect.con
cic:/Coq/Init/Specif/sigS_ind.con
cic:/Coq/Init/Specif/sigS_rec.con
cic:/Coq/Init/Specif/sigS_rect.con
cic:/Coq/Init/Specif/sigT_ind.con
cic:/Coq/Init/Specif/sigT_rec.con
cic:/Coq/Init/Specif/sigT_rect.con
cic:/Coq/Init/Specif/sig_ind.con
cic:/Coq/Init/Specif/sig_rec.con
cic:/Coq/Init/Specif/sig_rect.con
cic:/Coq/Init/Specif/sumbool_ind.con
cic:/Coq/Init/Specif/sumbool_rec.con
cic:/Coq/Init/Specif/sumbool_rect.con
cic:/Coq/Init/Specif/sumor_ind.con
cic:/Coq/Init/Specif/sumor_rec.con
cic:/Coq/Init/Specif/sumor_rect.con
cic:/Coq/Init/Specif/value.con
cic:/Coq/Init/Wf/Acc_ind.con
cic:/Coq/Init/Wf/Acc_inv.con
cic:/Coq/Init/Wf/Acc_inv_dep.con
cic:/Coq/Init/Wf/Acc_iter.con
cic:/Coq/Init/Wf/Acc_iter_2.con
cic:/Coq/Init/Wf/Acc_rec.con
cic:/Coq/Init/Wf/Acc_rect.con
cic:/Coq/Init/Wf/Fix.con
cic:/Coq/Init/Wf/Fix_F.con
cic:/Coq/Init/Wf/Fix_F_eq.con
cic:/Coq/Init/Wf/Fix_F_inv.con
cic:/Coq/Init/Wf/Fix_eq.con
cic:/Coq/Init/Wf/well_founded.con
cic:/Coq/Init/Wf/well_founded_ind.con
cic:/Coq/Init/Wf/well_founded_induction.con
cic:/Coq/Init/Wf/well_founded_induction_type.con
cic:/Coq/Init/Wf/well_founded_induction_type_2.con
cic:/Coq/Lists/List/In.con
cic:/Coq/Lists/List/In_dec.con
cic:/Coq/Lists/List/app.con
cic:/Coq/Lists/List/app_ass.con
cic:/Coq/Lists/List/app_comm_cons.con
cic:/Coq/Lists/List/app_cons_not_nil.con
cic:/Coq/Lists/List/app_eq_nil.con
cic:/Coq/Lists/List/app_eq_unit.con
cic:/Coq/Lists/List/app_inj_tail.con
cic:/Coq/Lists/List/app_nil_end.con
cic:/Coq/Lists/List/ass_app.con
cic:/Coq/Lists/List/distr_rev.con
cic:/Coq/Lists/List/flat_map.con
cic:/Coq/Lists/List/fold_left.con
cic:/Coq/Lists/List/fold_right.con
cic:/Coq/Lists/List/fold_symmetric.con
cic:/Coq/Lists/List/head.con
cic:/Coq/Lists/List/in_app_or.con
cic:/Coq/Lists/List/in_cons.con
cic:/Coq/Lists/List/in_eq.con
cic:/Coq/Lists/List/in_inv.con
cic:/Coq/Lists/List/in_map.con
cic:/Coq/Lists/List/in_nil.con
cic:/Coq/Lists/List/in_or_app.con
cic:/Coq/Lists/List/in_prod.con
cic:/Coq/Lists/List/in_prod_aux.con
cic:/Coq/Lists/List/incl.con
cic:/Coq/Lists/List/incl_app.con
cic:/Coq/Lists/List/incl_appl.con
cic:/Coq/Lists/List/incl_appr.con
cic:/Coq/Lists/List/incl_cons.con
cic:/Coq/Lists/List/incl_refl.con
cic:/Coq/Lists/List/incl_tl.con
cic:/Coq/Lists/List/incl_tran.con
cic:/Coq/Lists/List/lel.con
cic:/Coq/Lists/List/lel_cons.con
cic:/Coq/Lists/List/lel_cons_cons.con
cic:/Coq/Lists/List/lel_nil.con
cic:/Coq/Lists/List/lel_refl.con
cic:/Coq/Lists/List/lel_tail.con
cic:/Coq/Lists/List/lel_trans.con
cic:/Coq/Lists/List/length.con
cic:/Coq/Lists/List/list_eq_dec.con
cic:/Coq/Lists/List/list_ind.con
cic:/Coq/Lists/List/list_power.con
cic:/Coq/Lists/List/list_prod.con
cic:/Coq/Lists/List/list_rec.con
cic:/Coq/Lists/List/list_rect.con
cic:/Coq/Lists/List/map.con
cic:/Coq/Lists/List/nil_cons.con
cic:/Coq/Lists/List/nth.con
cic:/Coq/Lists/List/nth_In.con
cic:/Coq/Lists/List/nth_S_cons.con
cic:/Coq/Lists/List/nth_default.con
cic:/Coq/Lists/List/nth_error.con
cic:/Coq/Lists/List/nth_in_or_default.con
cic:/Coq/Lists/List/nth_ok.con
cic:/Coq/Lists/List/rev.con
cic:/Coq/Lists/List/rev_ind.con
cic:/Coq/Lists/List/rev_involutive.con
cic:/Coq/Lists/List/rev_list_ind.con
cic:/Coq/Lists/List/rev_unit.con
cic:/Coq/Lists/List/tail.con
cic:/Coq/Lists/ListSet/empty_set.con
cic:/Coq/Lists/ListSet/set.con
cic:/Coq/Lists/ListSet/set_In.con
cic:/Coq/Lists/ListSet/set_In_dec.con
cic:/Coq/Lists/ListSet/set_add.con
cic:/Coq/Lists/ListSet/set_add_elim.con
cic:/Coq/Lists/ListSet/set_add_elim2.con
cic:/Coq/Lists/ListSet/set_add_intro.con
cic:/Coq/Lists/ListSet/set_add_intro1.con
cic:/Coq/Lists/ListSet/set_add_intro2.con
cic:/Coq/Lists/ListSet/set_add_not_empty.con
cic:/Coq/Lists/ListSet/set_diff.con
cic:/Coq/Lists/ListSet/set_diff_elim1.con
cic:/Coq/Lists/ListSet/set_diff_elim2.con
cic:/Coq/Lists/ListSet/set_diff_intro.con
cic:/Coq/Lists/ListSet/set_diff_trivial.con
cic:/Coq/Lists/ListSet/set_fold_left.con
cic:/Coq/Lists/ListSet/set_fold_right.con
cic:/Coq/Lists/ListSet/set_inter.con
cic:/Coq/Lists/ListSet/set_inter_elim.con
cic:/Coq/Lists/ListSet/set_inter_elim1.con
cic:/Coq/Lists/ListSet/set_inter_elim2.con
cic:/Coq/Lists/ListSet/set_inter_intro.con
cic:/Coq/Lists/ListSet/set_map.con
cic:/Coq/Lists/ListSet/set_mem.con
cic:/Coq/Lists/ListSet/set_mem_complete1.con
cic:/Coq/Lists/ListSet/set_mem_complete2.con
cic:/Coq/Lists/ListSet/set_mem_correct1.con
cic:/Coq/Lists/ListSet/set_mem_correct2.con
cic:/Coq/Lists/ListSet/set_mem_ind.con
cic:/Coq/Lists/ListSet/set_mem_ind2.con
cic:/Coq/Lists/ListSet/set_power.con
cic:/Coq/Lists/ListSet/set_prod.con
cic:/Coq/Lists/ListSet/set_remove.con
cic:/Coq/Lists/ListSet/set_union.con
cic:/Coq/Lists/ListSet/set_union_elim.con
cic:/Coq/Lists/ListSet/set_union_emptyL.con
cic:/Coq/Lists/ListSet/set_union_emptyR.con
cic:/Coq/Lists/ListSet/set_union_intro.con
cic:/Coq/Lists/ListSet/set_union_intro1.con
cic:/Coq/Lists/ListSet/set_union_intro2.con
cic:/Coq/Lists/MonoList/A.con
cic:/Coq/Lists/MonoList/In.con
cic:/Coq/Lists/MonoList/List_Dom.con
cic:/Coq/Lists/MonoList/app.con
cic:/Coq/Lists/MonoList/app_ass.con
cic:/Coq/Lists/MonoList/app_nil_end.con
cic:/Coq/Lists/MonoList/ass_app.con
cic:/Coq/Lists/MonoList/in_app_or.con
cic:/Coq/Lists/MonoList/in_cons.con
cic:/Coq/Lists/MonoList/in_eq.con
cic:/Coq/Lists/MonoList/in_or_app.con
cic:/Coq/Lists/MonoList/incl.con
cic:/Coq/Lists/MonoList/incl_app.con
cic:/Coq/Lists/MonoList/incl_appl.con
cic:/Coq/Lists/MonoList/incl_appr.con
cic:/Coq/Lists/MonoList/incl_cons.con
cic:/Coq/Lists/MonoList/incl_refl.con
cic:/Coq/Lists/MonoList/incl_tl.con
cic:/Coq/Lists/MonoList/incl_tran.con
cic:/Coq/Lists/MonoList/lel.con
cic:/Coq/Lists/MonoList/lel_cons.con
cic:/Coq/Lists/MonoList/lel_cons_cons.con
cic:/Coq/Lists/MonoList/lel_nil.con
cic:/Coq/Lists/MonoList/lel_refl.con
cic:/Coq/Lists/MonoList/lel_tail.con
cic:/Coq/Lists/MonoList/lel_trans.con
cic:/Coq/Lists/MonoList/length.con
cic:/Coq/Lists/MonoList/list_ind.con
cic:/Coq/Lists/MonoList/list_rec.con
cic:/Coq/Lists/MonoList/list_rect.con
cic:/Coq/Lists/MonoList/nil_cons.con
cic:/Coq/Lists/MonoList/tail.con
cic:/Coq/Lists/Streams/EqSt_reflex.con
cic:/Coq/Lists/Streams/Exists_ind.con
cic:/Coq/Lists/Streams/ForAll_coind.con
cic:/Coq/Lists/Streams/Str_nth.con
cic:/Coq/Lists/Streams/Str_nth_plus.con
cic:/Coq/Lists/Streams/Str_nth_tl.con
cic:/Coq/Lists/Streams/Str_nth_tl_plus.con
cic:/Coq/Lists/Streams/const.con
cic:/Coq/Lists/Streams/eqst_ntheq.con
cic:/Coq/Lists/Streams/hd.con
cic:/Coq/Lists/Streams/map.con
cic:/Coq/Lists/Streams/ntheq_eqst.con
cic:/Coq/Lists/Streams/sym_EqSt.con
cic:/Coq/Lists/Streams/tl.con
cic:/Coq/Lists/Streams/tl_nth_tl.con
cic:/Coq/Lists/Streams/trans_EqSt.con
cic:/Coq/Lists/Streams/unfold_Stream.con
cic:/Coq/Lists/TheoryList/AllS_assoc_ind.con
cic:/Coq/Lists/TheoryList/AllS_ind.con
cic:/Coq/Lists/TheoryList/Assoc.con
cic:/Coq/Lists/TheoryList/Find.con
cic:/Coq/Lists/TheoryList/Hd.con
cic:/Coq/Lists/TheoryList/InR_INV.con
cic:/Coq/Lists/TheoryList/InR_app_or.con
cic:/Coq/Lists/TheoryList/InR_cons_inv.con
cic:/Coq/Lists/TheoryList/InR_ind.con
cic:/Coq/Lists/TheoryList/InR_inv.con
cic:/Coq/Lists/TheoryList/InR_or_app.con
cic:/Coq/Lists/TheoryList/In_In_spec.con
cic:/Coq/Lists/TheoryList/In_spec_ind.con
cic:/Coq/Lists/TheoryList/Index.con
cic:/Coq/Lists/TheoryList/Index_p.con
cic:/Coq/Lists/TheoryList/Isnil.con
cic:/Coq/Lists/TheoryList/Isnil_dec.con
cic:/Coq/Lists/TheoryList/Isnil_nil.con
cic:/Coq/Lists/TheoryList/Item.con
cic:/Coq/Lists/TheoryList/Length.con
cic:/Coq/Lists/TheoryList/Length_l.con
cic:/Coq/Lists/TheoryList/Length_l_pf.con
cic:/Coq/Lists/TheoryList/Mem.con
cic:/Coq/Lists/TheoryList/Nth.con
cic:/Coq/Lists/TheoryList/Nth_func.con
cic:/Coq/Lists/TheoryList/Tl.con
cic:/Coq/Lists/TheoryList/Try_find.con
cic:/Coq/Lists/TheoryList/Uncons.con
cic:/Coq/Lists/TheoryList/assoc.con
cic:/Coq/Lists/TheoryList/find.con
cic:/Coq/Lists/TheoryList/fst_nth_nth.con
cic:/Coq/Lists/TheoryList/fst_nth_spec_ind.con
cic:/Coq/Lists/TheoryList/index_p.con
cic:/Coq/Lists/TheoryList/mem.con
cic:/Coq/Lists/TheoryList/not_Isnil_cons.con
cic:/Coq/Lists/TheoryList/nth_le_length.con
cic:/Coq/Lists/TheoryList/nth_lt_O.con
cic:/Coq/Lists/TheoryList/nth_spec_ind.con
cic:/Coq/Lists/TheoryList/try_find.con
cic:/Coq/Logic/Berardi/AC.con
cic:/Coq/Logic/Berardi/AC_IF.con
cic:/Coq/Logic/Berardi/IFProp.con
cic:/Coq/Logic/Berardi/L1.con
cic:/Coq/Logic/Berardi/Not_b.con
cic:/Coq/Logic/Berardi/R.con
cic:/Coq/Logic/Berardi/U.con
cic:/Coq/Logic/Berardi/classical_proof_irrelevence.con
cic:/Coq/Logic/Berardi/f.con
cic:/Coq/Logic/Berardi/g.con
cic:/Coq/Logic/Berardi/i.con
cic:/Coq/Logic/Berardi/i2.con
cic:/Coq/Logic/Berardi/inv.con
cic:/Coq/Logic/Berardi/inv2.con
cic:/Coq/Logic/Berardi/j.con
cic:/Coq/Logic/Berardi/j2.con
cic:/Coq/Logic/Berardi/not_has_fixpoint.con
cic:/Coq/Logic/Berardi/pow.con
cic:/Coq/Logic/Berardi/retract_cond_ind.con
cic:/Coq/Logic/Berardi/retract_cond_rec.con
cic:/Coq/Logic/Berardi/retract_cond_rect.con
cic:/Coq/Logic/Berardi/retract_ind.con
cic:/Coq/Logic/Berardi/retract_pow_U_U.con
cic:/Coq/Logic/Berardi/retract_rec.con
cic:/Coq/Logic/Berardi/retract_rect.con
cic:/Coq/Logic/ChoiceFacts/FunChoice_Equiv_RelChoice_and_ParamDefinDescr.con
cic:/Coq/Logic/ChoiceFacts/FunctionalChoice.con
cic:/Coq/Logic/ChoiceFacts/GuardedRelationalChoice.con
cic:/Coq/Logic/ChoiceFacts/IndependenceOfPremises.con
cic:/Coq/Logic/ChoiceFacts/ParamDefiniteDescription.con
cic:/Coq/Logic/ChoiceFacts/ProofIrrelevance.con
cic:/Coq/Logic/ChoiceFacts/RelationalChoice.con
cic:/Coq/Logic/ChoiceFacts/description_rel_choice_imp_funct_choice.con
cic:/Coq/Logic/ChoiceFacts/funct_choice_imp_description.con
cic:/Coq/Logic/ChoiceFacts/funct_choice_imp_rel_choice.con
cic:/Coq/Logic/ChoiceFacts/rel_choice_and_proof_irrel_imp_guarded_rel_choice.con
cic:/Coq/Logic/ChoiceFacts/rel_choice_indep_of_premises_imp_guarded_rel_choice.con
cic:/Coq/Logic/ClassicalChoice/choice.con
cic:/Coq/Logic/ClassicalDescription/classic_set.con
cic:/Coq/Logic/ClassicalDescription/dependent_description.con
cic:/Coq/Logic/ClassicalDescription/description.con
cic:/Coq/Logic/ClassicalFacts/BoolP.con
cic:/Coq/Logic/ClassicalFacts/BoolP_dep_induction.con
cic:/Coq/Logic/ClassicalFacts/BoolP_elim.con
cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redl.con
cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redr.con
cic:/Coq/Logic/ClassicalFacts/F.con
cic:/Coq/Logic/ClassicalFacts/FalseP.con
cic:/Coq/Logic/ClassicalFacts/Fix.con
cic:/Coq/Logic/ClassicalFacts/TrueP.con
cic:/Coq/Logic/ClassicalFacts/aux.con
cic:/Coq/Logic/ClassicalFacts/boolP_elim_redl.con
cic:/Coq/Logic/ClassicalFacts/boolP_elim_redr.con
cic:/Coq/Logic/ClassicalFacts/boolP_ind.con
cic:/Coq/Logic/ClassicalFacts/boolP_indd.con
cic:/Coq/Logic/ClassicalFacts/excluded_middle.con
cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cc.con
cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cic.con
cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_gen.con
cic:/Coq/Logic/ClassicalFacts/ext_prop_fixpoint.con
cic:/Coq/Logic/ClassicalFacts/f1.con
cic:/Coq/Logic/ClassicalFacts/f1_o_f2.con
cic:/Coq/Logic/ClassicalFacts/f2.con
cic:/Coq/Logic/ClassicalFacts/has_fixpoint_ind.con
cic:/Coq/Logic/ClassicalFacts/has_fixpoint_rec.con
cic:/Coq/Logic/ClassicalFacts/has_fixpoint_rect.con
cic:/Coq/Logic/ClassicalFacts/inhabited.con
cic:/Coq/Logic/ClassicalFacts/proof_irrelevance.con
cic:/Coq/Logic/ClassicalFacts/prop_degen_em.con
cic:/Coq/Logic/ClassicalFacts/prop_degen_ext.con
cic:/Coq/Logic/ClassicalFacts/prop_degeneracy.con
cic:/Coq/Logic/ClassicalFacts/prop_ext_A_eq_A_imp_A.con
cic:/Coq/Logic/ClassicalFacts/prop_ext_em_degen.con
cic:/Coq/Logic/ClassicalFacts/prop_ext_retract_A_A_imp_A.con
cic:/Coq/Logic/ClassicalFacts/prop_extensionality.con
cic:/Coq/Logic/ClassicalFacts/retract_ind.con
cic:/Coq/Logic/ClassicalFacts/retract_rec.con
cic:/Coq/Logic/ClassicalFacts/retract_rect.con
cic:/Coq/Logic/Classical_Pred_Set/all_not_not_ex.con
cic:/Coq/Logic/Classical_Pred_Set/ex_not_not_all.con
cic:/Coq/Logic/Classical_Pred_Set/not_all_ex_not.con
cic:/Coq/Logic/Classical_Pred_Set/not_all_not_ex.con
cic:/Coq/Logic/Classical_Pred_Set/not_ex_all_not.con
cic:/Coq/Logic/Classical_Pred_Set/not_ex_not_all.con
cic:/Coq/Logic/Classical_Pred_Type/all_not_not_ex.con
cic:/Coq/Logic/Classical_Pred_Type/ex_not_not_all.con
cic:/Coq/Logic/Classical_Pred_Type/not_all_ex_not.con
cic:/Coq/Logic/Classical_Pred_Type/not_all_not_ex.con
cic:/Coq/Logic/Classical_Pred_Type/not_ex_all_not.con
cic:/Coq/Logic/Classical_Pred_Type/not_ex_not_all.con
cic:/Coq/Logic/Classical_Prop/NNPP.con
cic:/Coq/Logic/Classical_Prop/and_not_or.con
cic:/Coq/Logic/Classical_Prop/classic.con
cic:/Coq/Logic/Classical_Prop/imply_and_or.con
cic:/Coq/Logic/Classical_Prop/imply_and_or2.con
cic:/Coq/Logic/Classical_Prop/imply_to_and.con
cic:/Coq/Logic/Classical_Prop/imply_to_or.con
cic:/Coq/Logic/Classical_Prop/not_and_or.con
cic:/Coq/Logic/Classical_Prop/not_imply_elim.con
cic:/Coq/Logic/Classical_Prop/not_imply_elim2.con
cic:/Coq/Logic/Classical_Prop/not_or_and.con
cic:/Coq/Logic/Classical_Prop/or_not_and.con
cic:/Coq/Logic/Classical_Prop/or_to_imply.con
cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con
cic:/Coq/Logic/Decidable/dec_False.con
cic:/Coq/Logic/Decidable/dec_True.con
cic:/Coq/Logic/Decidable/dec_and.con
cic:/Coq/Logic/Decidable/dec_imp.con
cic:/Coq/Logic/Decidable/dec_not.con
cic:/Coq/Logic/Decidable/dec_not_not.con
cic:/Coq/Logic/Decidable/dec_or.con
cic:/Coq/Logic/Decidable/decidable.con
cic:/Coq/Logic/Decidable/imp_simp.con
cic:/Coq/Logic/Decidable/not_and.con
cic:/Coq/Logic/Decidable/not_imp.con
cic:/Coq/Logic/Decidable/not_not.con
cic:/Coq/Logic/Decidable/not_or.con
cic:/Coq/Logic/Diaconescu/AC.con
cic:/Coq/Logic/Diaconescu/PredicateExtensionality.con
cic:/Coq/Logic/Diaconescu/guarded_rel_choice.con
cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con
cic:/Coq/Logic/Diaconescu/proof_irrel.con
cic:/Coq/Logic/Diaconescu/prop_ext.con
cic:/Coq/Logic/Eqdep/Streicher_K.con
cic:/Coq/Logic/Eqdep/UIP.con
cic:/Coq/Logic/Eqdep/UIP_refl.con
cic:/Coq/Logic/Eqdep/eq_dep1_dep.con
cic:/Coq/Logic/Eqdep/eq_dep1_eq.con
cic:/Coq/Logic/Eqdep/eq_dep1_ind.con
cic:/Coq/Logic/Eqdep/eq_dep1_rec.con
cic:/Coq/Logic/Eqdep/eq_dep1_rect.con
cic:/Coq/Logic/Eqdep/eq_dep_dep1.con
cic:/Coq/Logic/Eqdep/eq_dep_eq.con
cic:/Coq/Logic/Eqdep/eq_dep_ind.con
cic:/Coq/Logic/Eqdep/eq_dep_rec.con
cic:/Coq/Logic/Eqdep/eq_dep_rect.con
cic:/Coq/Logic/Eqdep/eq_dep_sym.con
cic:/Coq/Logic/Eqdep/eq_dep_trans.con
cic:/Coq/Logic/Eqdep/eq_indd.con
cic:/Coq/Logic/Eqdep/eq_rec_eq.con
cic:/Coq/Logic/Eqdep/eq_rect_eq.con
cic:/Coq/Logic/Eqdep/equiv_eqex_eqdep.con
cic:/Coq/Logic/Eqdep/inj_pair2.con
cic:/Coq/Logic/Eqdep/inj_pairT2.con
cic:/Coq/Logic/Eqdep_dec/K_dec.con
cic:/Coq/Logic/Eqdep_dec/K_dec_set.con
cic:/Coq/Logic/Eqdep_dec/eq2eqT.con
cic:/Coq/Logic/Eqdep_dec/eqT2eq.con
cic:/Coq/Logic/Eqdep_dec/eqT_eq_bij.con
cic:/Coq/Logic/Eqdep_dec/eq_eqT_bij.con
cic:/Coq/Logic/Eqdep_dec/eq_proofs_unicity.con
cic:/Coq/Logic/Eqdep_dec/inj_right_pair.con
cic:/Coq/Logic/Eqdep_dec/nu_left_inv.con
cic:/Coq/Logic/Eqdep_dec/trans_sym_eqT.con
cic:/Coq/Logic/Hurkens/I.con
cic:/Coq/Logic/Hurkens/Omega.con
cic:/Coq/Logic/Hurkens/U.con
cic:/Coq/Logic/Hurkens/V.con
cic:/Coq/Logic/Hurkens/WF.con
cic:/Coq/Logic/Hurkens/induct.con
cic:/Coq/Logic/Hurkens/le.con
cic:/Coq/Logic/Hurkens/lemma1.con
cic:/Coq/Logic/Hurkens/lemma2.con
cic:/Coq/Logic/Hurkens/paradox.con
cic:/Coq/Logic/Hurkens/sb.con
cic:/Coq/Logic/JMeq/JMeq_eq.con
cic:/Coq/Logic/JMeq/JMeq_eq_dep.con
cic:/Coq/Logic/JMeq/JMeq_ind.con
cic:/Coq/Logic/JMeq/JMeq_ind_r.con
cic:/Coq/Logic/JMeq/JMeq_rec.con
cic:/Coq/Logic/JMeq/JMeq_rec_r.con
cic:/Coq/Logic/JMeq/JMeq_rect.con
cic:/Coq/Logic/JMeq/eq_dep_JMeq.con
cic:/Coq/Logic/JMeq/sym_JMeq.con
cic:/Coq/Logic/JMeq/trans_JMeq.con
cic:/Coq/Logic/ProofIrrelevance/b2p.con
cic:/Coq/Logic/ProofIrrelevance/or_elim_redl.con
cic:/Coq/Logic/ProofIrrelevance/or_elim_redr.con
cic:/Coq/Logic/ProofIrrelevance/or_indd.con
cic:/Coq/Logic/ProofIrrelevance/p2b.con
cic:/Coq/Logic/ProofIrrelevance/p2p1.con
cic:/Coq/Logic/ProofIrrelevance/p2p2.con
cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cc.con
cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con
cic:/Coq/Logic/RelationalChoice/relational_choice.con
cic:/Coq/NArith/BinNat/N_ind.con
cic:/Coq/NArith/BinNat/N_rec.con
cic:/Coq/NArith/BinNat/N_rect.con
cic:/Coq/NArith/BinNat/Ncompare.con
cic:/Coq/NArith/BinNat/Ncompare_Eq_eq.con
cic:/Coq/NArith/BinNat/Ndouble.con
cic:/Coq/NArith/BinNat/Ndouble_plus_one.con
cic:/Coq/NArith/BinNat/Nind.con
cic:/Coq/NArith/BinNat/Nmult.con
cic:/Coq/NArith/BinNat/Nmult_0_l.con
cic:/Coq/NArith/BinNat/Nmult_1_l.con
cic:/Coq/NArith/BinNat/Nmult_1_r.con
cic:/Coq/NArith/BinNat/Nmult_assoc.con
cic:/Coq/NArith/BinNat/Nmult_comm.con
cic:/Coq/NArith/BinNat/Nmult_plus_distr_r.con
cic:/Coq/NArith/BinNat/Nmult_reg_r.con
cic:/Coq/NArith/BinNat/Nplus.con
cic:/Coq/NArith/BinNat/Nplus_0_l.con
cic:/Coq/NArith/BinNat/Nplus_0_r.con
cic:/Coq/NArith/BinNat/Nplus_assoc.con
cic:/Coq/NArith/BinNat/Nplus_comm.con
cic:/Coq/NArith/BinNat/Nplus_reg_l.con
cic:/Coq/NArith/BinNat/Nplus_succ.con
cic:/Coq/NArith/BinNat/Nsucc.con
cic:/Coq/NArith/BinNat/Nsucc_inj.con
cic:/Coq/NArith/BinPos/Dcompare.con
cic:/Coq/NArith/BinPos/P_of_succ_nat.con
cic:/Coq/NArith/BinPos/Pcase.con
cic:/Coq/NArith/BinPos/Pcompare.con
cic:/Coq/NArith/BinPos/Pcompare_Eq_eq.con
cic:/Coq/NArith/BinPos/Pcompare_Gt_Gt.con
cic:/Coq/NArith/BinPos/Pcompare_Gt_Lt.con
cic:/Coq/NArith/BinPos/Pcompare_Lt_Gt.con
cic:/Coq/NArith/BinPos/Pcompare_Lt_Lt.con
cic:/Coq/NArith/BinPos/Pcompare_antisym.con
cic:/Coq/NArith/BinPos/Pcompare_not_Eq.con
cic:/Coq/NArith/BinPos/Pcompare_refl.con
cic:/Coq/NArith/BinPos/Pdiv2.con
cic:/Coq/NArith/BinPos/Pdouble_mask.con
cic:/Coq/NArith/BinPos/Pdouble_minus_one.con
cic:/Coq/NArith/BinPos/Pdouble_minus_one_o_succ_eq_xI.con
cic:/Coq/NArith/BinPos/Pdouble_minus_two.con
cic:/Coq/NArith/BinPos/Pdouble_plus_one_mask.con
cic:/Coq/NArith/BinPos/Pind.con
cic:/Coq/NArith/BinPos/Pminus.con
cic:/Coq/NArith/BinPos/Pminus_mask.con
cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
cic:/Coq/NArith/BinPos/Pminus_mask_carry.con
cic:/Coq/NArith/BinPos/Pminus_mask_diag.con
cic:/Coq/NArith/BinPos/Pmult.con
cic:/Coq/NArith/BinPos/Pmult_1_inversion_l.con
cic:/Coq/NArith/BinPos/Pmult_1_r.con
cic:/Coq/NArith/BinPos/Pmult_assoc.con
cic:/Coq/NArith/BinPos/Pmult_comm.con
cic:/Coq/NArith/BinPos/Pmult_nat.con
cic:/Coq/NArith/BinPos/Pmult_plus_distr_l.con
cic:/Coq/NArith/BinPos/Pmult_plus_distr_r.con
cic:/Coq/NArith/BinPos/Pmult_reg_l.con
cic:/Coq/NArith/BinPos/Pmult_reg_r.con
cic:/Coq/NArith/BinPos/Pmult_xI_mult_xO_discr.con
cic:/Coq/NArith/BinPos/Pmult_xI_permute_r.con
cic:/Coq/NArith/BinPos/Pmult_xO_discr.con
cic:/Coq/NArith/BinPos/Pmult_xO_permute_r.con
cic:/Coq/NArith/BinPos/Pplus.con
cic:/Coq/NArith/BinPos/Pplus_assoc.con
cic:/Coq/NArith/BinPos/Pplus_carry.con
cic:/Coq/NArith/BinPos/Pplus_carry_no_neutral.con
cic:/Coq/NArith/BinPos/Pplus_carry_plus.con
cic:/Coq/NArith/BinPos/Pplus_carry_pred_eq_plus.con
cic:/Coq/NArith/BinPos/Pplus_carry_reg_l.con
cic:/Coq/NArith/BinPos/Pplus_carry_reg_r.con
cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
cic:/Coq/NArith/BinPos/Pplus_comm.con
cic:/Coq/NArith/BinPos/Pplus_diag.con
cic:/Coq/NArith/BinPos/Pplus_minus.con
cic:/Coq/NArith/BinPos/Pplus_no_neutral.con
cic:/Coq/NArith/BinPos/Pplus_one_succ_l.con
cic:/Coq/NArith/BinPos/Pplus_one_succ_r.con
cic:/Coq/NArith/BinPos/Pplus_reg_l.con
cic:/Coq/NArith/BinPos/Pplus_reg_r.con
cic:/Coq/NArith/BinPos/Pplus_succ_permute_l.con
cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
cic:/Coq/NArith/BinPos/Pplus_xI_double_minus_one.con
cic:/Coq/NArith/BinPos/Pplus_xO_double_minus_one.con
cic:/Coq/NArith/BinPos/Ppred.con
cic:/Coq/NArith/BinPos/Ppred_succ.con
cic:/Coq/NArith/BinPos/Prec.con
cic:/Coq/NArith/BinPos/Psucc.con
cic:/Coq/NArith/BinPos/Psucc_discr.con
cic:/Coq/NArith/BinPos/Psucc_inj.con
cic:/Coq/NArith/BinPos/Psucc_not_one.con
cic:/Coq/NArith/BinPos/Psucc_o_double_minus_one_eq_xO.con
cic:/Coq/NArith/BinPos/Psucc_pred.con
cic:/Coq/NArith/BinPos/ZC1.con
cic:/Coq/NArith/BinPos/ZC2.con
cic:/Coq/NArith/BinPos/ZC3.con
cic:/Coq/NArith/BinPos/ZC4.con
cic:/Coq/NArith/BinPos/ZL10.con
cic:/Coq/NArith/BinPos/ZL11.con
cic:/Coq/NArith/BinPos/double_eq_one_discr.con
cic:/Coq/NArith/BinPos/double_eq_zero_inversion.con
cic:/Coq/NArith/BinPos/double_moins_un_xO_discr.con
cic:/Coq/NArith/BinPos/double_plus_one_eq_one_inversion.con
cic:/Coq/NArith/BinPos/double_plus_one_zero_discr.con
cic:/Coq/NArith/BinPos/iterate_add.con
cic:/Coq/NArith/BinPos/nat_of_P.con
cic:/Coq/NArith/BinPos/plus_iter.con
cic:/Coq/NArith/BinPos/plus_iter_eq_plus.con
cic:/Coq/NArith/BinPos/plus_iter_xI.con
cic:/Coq/NArith/BinPos/plus_iter_xO.con
cic:/Coq/NArith/BinPos/positive_ind.con
cic:/Coq/NArith/BinPos/positive_mask_ind.con
cic:/Coq/NArith/BinPos/positive_mask_rec.con
cic:/Coq/NArith/BinPos/positive_mask_rect.con
cic:/Coq/NArith/BinPos/positive_rec.con
cic:/Coq/NArith/BinPos/positive_rect.con
cic:/Coq/NArith/BinPos/xI_succ_xO.con
cic:/Coq/NArith/BinPos/xO_succ_permute.con
cic:/Coq/NArith/Pnat/P_of_succ_nat_o_nat_of_P_eq_succ.con
cic:/Coq/NArith/Pnat/Pcompare_minus_l.con
cic:/Coq/NArith/Pnat/Pcompare_minus_r.con
cic:/Coq/NArith/Pnat/Pmult_minus_distr_l.con
cic:/Coq/NArith/Pnat/Pmult_nat_2_mult_2_permute.con
cic:/Coq/NArith/Pnat/Pmult_nat_4_mult_2_permute.con
cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
cic:/Coq/NArith/Pnat/Pmult_nat_mult_permute.con
cic:/Coq/NArith/Pnat/Pmult_nat_plus_carry_morphism.con
cic:/Coq/NArith/Pnat/Pmult_nat_r_plus_morphism.con
cic:/Coq/NArith/Pnat/Pmult_nat_succ_morphism.con
cic:/Coq/NArith/Pnat/ZL16.con
cic:/Coq/NArith/Pnat/ZL17.con
cic:/Coq/NArith/Pnat/ZL3.con
cic:/Coq/NArith/Pnat/ZL4.con
cic:/Coq/NArith/Pnat/ZL5.con
cic:/Coq/NArith/Pnat/ZL6.con
cic:/Coq/NArith/Pnat/ZL7.con
cic:/Coq/NArith/Pnat/ZL8.con
cic:/Coq/NArith/Pnat/le_Pmult_nat.con
cic:/Coq/NArith/Pnat/lt_O_nat_of_P.con
cic:/Coq/NArith/Pnat/nat_of_P_gt_Gt_compare_complement_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_gt_Gt_compare_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_inj.con
cic:/Coq/NArith/Pnat/nat_of_P_lt_Lt_compare_complement_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_lt_Lt_compare_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_minus_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_mult_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_o_P_of_succ_nat_eq_succ.con
cic:/Coq/NArith/Pnat/nat_of_P_plus_carry_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_plus_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_succ_morphism.con
cic:/Coq/NArith/Pnat/nat_of_P_xH.con
cic:/Coq/NArith/Pnat/nat_of_P_xI.con
cic:/Coq/NArith/Pnat/nat_of_P_xO.con
cic:/Coq/NArith/Pnat/pred_o_P_of_succ_nat_o_nat_of_P_eq_id.con
cic:/Coq/Reals/ArithProp/euclidian_division.con
cic:/Coq/Reals/ArithProp/even_odd_cor.con
cic:/Coq/Reals/ArithProp/le_double.con
cic:/Coq/Reals/ArithProp/le_minusni_n.con
cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con
cic:/Coq/Reals/ArithProp/minus_neq_O.con
cic:/Coq/Reals/ArithProp/tech8.con
cic:/Coq/Reals/Binomial/C.con
cic:/Coq/Reals/Binomial/binomial.con
cic:/Coq/Reals/Binomial/pascal.con
cic:/Coq/Reals/Binomial/pascal_step1.con
cic:/Coq/Reals/Binomial/pascal_step2.con
cic:/Coq/Reals/Binomial/pascal_step3.con
cic:/Coq/Reals/Cauchy_prod/cauchy_finite.con
cic:/Coq/Reals/Cauchy_prod/sum_N_predN.con
cic:/Coq/Reals/Cauchy_prod/sum_plus.con
cic:/Coq/Reals/Cos_plus/Majxy.con
cic:/Coq/Reals/Cos_plus/Majxy_cv_R0.con
cic:/Coq/Reals/Cos_plus/cos_plus.con
cic:/Coq/Reals/Cos_plus/reste1_cv_R0.con
cic:/Coq/Reals/Cos_plus/reste1_maj.con
cic:/Coq/Reals/Cos_plus/reste2_cv_R0.con
cic:/Coq/Reals/Cos_plus/reste2_maj.con
cic:/Coq/Reals/Cos_plus/reste_cv_R0.con
cic:/Coq/Reals/Cos_rel/A1.con
cic:/Coq/Reals/Cos_rel/A1_cvg.con
cic:/Coq/Reals/Cos_rel/B1.con
cic:/Coq/Reals/Cos_rel/B1_cvg.con
cic:/Coq/Reals/Cos_rel/C1.con
cic:/Coq/Reals/Cos_rel/C1_cvg.con
cic:/Coq/Reals/Cos_rel/Reste.con
cic:/Coq/Reals/Cos_rel/Reste1.con
cic:/Coq/Reals/Cos_rel/Reste2.con
cic:/Coq/Reals/Cos_rel/cos_plus_form.con
cic:/Coq/Reals/Cos_rel/pow_sqr.con
cic:/Coq/Reals/DiscrR/IZR_eq.con
cic:/Coq/Reals/DiscrR/IZR_neq.con
cic:/Coq/Reals/DiscrR/Rlt_R0_R2.con
cic:/Coq/Reals/DiscrR/Rplus_lt_pos.con
cic:/Coq/Reals/Exp_prop/E1.con
cic:/Coq/Reals/Exp_prop/E1_cvg.con
cic:/Coq/Reals/Exp_prop/Reste_E.con
cic:/Coq/Reals/Exp_prop/Reste_E_cv.con
cic:/Coq/Reals/Exp_prop/Reste_E_maj.con
cic:/Coq/Reals/Exp_prop/Rle_Rinv.con
cic:/Coq/Reals/Exp_prop/derivable_pt_lim_exp_0.con
cic:/Coq/Reals/Exp_prop/div2_S_double.con
cic:/Coq/Reals/Exp_prop/div2_double.con
cic:/Coq/Reals/Exp_prop/div2_not_R0.con
cic:/Coq/Reals/Exp_prop/exp_form.con
cic:/Coq/Reals/Exp_prop/exp_plus.con
cic:/Coq/Reals/Exp_prop/exp_pos.con
cic:/Coq/Reals/Exp_prop/exp_pos_pos.con
cic:/Coq/Reals/Exp_prop/maj_Reste_E.con
cic:/Coq/Reals/Exp_prop/maj_Reste_cv_R0.con
cic:/Coq/Reals/MVT/IAF.con
cic:/Coq/Reals/MVT/IAF_var.con
cic:/Coq/Reals/MVT/MVT.con
cic:/Coq/Reals/MVT/MVT_cor1.con
cic:/Coq/Reals/MVT/MVT_cor2.con
cic:/Coq/Reals/MVT/MVT_cor3.con
cic:/Coq/Reals/MVT/Rolle.con
cic:/Coq/Reals/MVT/antiderivative_Ucte.con
cic:/Coq/Reals/MVT/derive_increasing_interv.con
cic:/Coq/Reals/MVT/derive_increasing_interv_ax.con
cic:/Coq/Reals/MVT/derive_increasing_interv_var.con
cic:/Coq/Reals/MVT/increasing_decreasing.con
cic:/Coq/Reals/MVT/increasing_decreasing_opp.con
cic:/Coq/Reals/MVT/negative_derivative.con
cic:/Coq/Reals/MVT/nonneg_derivative_1.con
cic:/Coq/Reals/MVT/nonpos_derivative_0.con
cic:/Coq/Reals/MVT/nonpos_derivative_1.con
cic:/Coq/Reals/MVT/null_derivative_0.con
cic:/Coq/Reals/MVT/null_derivative_1.con
cic:/Coq/Reals/MVT/null_derivative_loc.con
cic:/Coq/Reals/MVT/positive_derivative.con
cic:/Coq/Reals/MVT/strictincreasing_strictdecreasing_opp.con
cic:/Coq/Reals/NewtonInt/FTCN_step1.con
cic:/Coq/Reals/NewtonInt/FTC_Newton.con
cic:/Coq/Reals/NewtonInt/NewtonInt.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P1.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P2.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P3.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P4.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P5.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P6.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P7.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P8.con
cic:/Coq/Reals/NewtonInt/NewtonInt_P9.con
cic:/Coq/Reals/NewtonInt/Newton_integrable.con
cic:/Coq/Reals/NewtonInt/antiderivative_P1.con
cic:/Coq/Reals/NewtonInt/antiderivative_P2.con
cic:/Coq/Reals/NewtonInt/antiderivative_P3.con
cic:/Coq/Reals/NewtonInt/antiderivative_P4.con
cic:/Coq/Reals/PartSum/Cauchy_crit_series.con
cic:/Coq/Reals/PartSum/Rabs_triang_gen.con
cic:/Coq/Reals/PartSum/Rsum_abs.con
cic:/Coq/Reals/PartSum/SP.con
cic:/Coq/Reals/PartSum/cauchy_abs.con
cic:/Coq/Reals/PartSum/cond_pos_sum.con
cic:/Coq/Reals/PartSum/cv_cauchy_1.con
cic:/Coq/Reals/PartSum/cv_cauchy_2.con
cic:/Coq/Reals/PartSum/decomp_sum.con
cic:/Coq/Reals/PartSum/minus_sum.con
cic:/Coq/Reals/PartSum/plus_sum.con
cic:/Coq/Reals/PartSum/scal_sum.con
cic:/Coq/Reals/PartSum/sum_Rle.con
cic:/Coq/Reals/PartSum/sum_cte.con
cic:/Coq/Reals/PartSum/sum_cv_maj.con
cic:/Coq/Reals/PartSum/sum_decomposition.con
cic:/Coq/Reals/PartSum/sum_eq.con
cic:/Coq/Reals/PartSum/sum_eq_R0.con
cic:/Coq/Reals/PartSum/sum_growing.con
cic:/Coq/Reals/PartSum/sum_incr.con
cic:/Coq/Reals/PartSum/tech1.con
cic:/Coq/Reals/PartSum/tech11.con
cic:/Coq/Reals/PartSum/tech12.con
cic:/Coq/Reals/PartSum/tech2.con
cic:/Coq/Reals/PartSum/tech3.con
cic:/Coq/Reals/PartSum/tech4.con
cic:/Coq/Reals/PartSum/tech5.con
cic:/Coq/Reals/PartSum/tech6.con
cic:/Coq/Reals/PartSum/tech7.con
cic:/Coq/Reals/PartSum/uniqueness_sum.con
cic:/Coq/Reals/RIneq/INR_IZR_INZ.con
cic:/Coq/Reals/RIneq/INR_eq.con
cic:/Coq/Reals/RIneq/INR_le.con
cic:/Coq/Reals/RIneq/INR_lt.con
cic:/Coq/Reals/RIneq/INR_lt_1.con
cic:/Coq/Reals/RIneq/INR_pos.con
cic:/Coq/Reals/RIneq/IZN.con
cic:/Coq/Reals/RIneq/IZR_ge.con
cic:/Coq/Reals/RIneq/IZR_le.con
cic:/Coq/Reals/RIneq/IZR_lt.con
cic:/Coq/Reals/RIneq/RTheory.con
cic:/Coq/Reals/RIneq/Rdichotomy.con
cic:/Coq/Reals/RIneq/Req_dec.con
cic:/Coq/Reals/RIneq/Req_ge.con
cic:/Coq/Reals/RIneq/Req_ge_sym.con
cic:/Coq/Reals/RIneq/Req_le.con
cic:/Coq/Reals/RIneq/Req_le_sym.con
cic:/Coq/Reals/RIneq/Rge_antisym.con
cic:/Coq/Reals/RIneq/Rge_dec.con
cic:/Coq/Reals/RIneq/Rge_gt_trans.con
cic:/Coq/Reals/RIneq/Rge_le.con
cic:/Coq/Reals/RIneq/Rge_minus.con
cic:/Coq/Reals/RIneq/Rge_trans.con
cic:/Coq/Reals/RIneq/Rgt_dec.con
cic:/Coq/Reals/RIneq/Rgt_ge.con
cic:/Coq/Reals/RIneq/Rgt_ge_trans.con
cic:/Coq/Reals/RIneq/Rgt_minus.con
cic:/Coq/Reals/RIneq/Rgt_not_eq.con
cic:/Coq/Reals/RIneq/Rgt_not_le.con
cic:/Coq/Reals/RIneq/Rgt_trans.con
cic:/Coq/Reals/RIneq/Rinv_0_lt_compat.con
cic:/Coq/Reals/RIneq/Rinv_1.con
cic:/Coq/Reals/RIneq/Rinv_1_lt_contravar.con
cic:/Coq/Reals/RIneq/Rinv_involutive.con
cic:/Coq/Reals/RIneq/Rinv_l_sym.con
cic:/Coq/Reals/RIneq/Rinv_lt_0_compat.con
cic:/Coq/Reals/RIneq/Rinv_lt_contravar.con
cic:/Coq/Reals/RIneq/Rinv_mult_distr.con
cic:/Coq/Reals/RIneq/Rinv_mult_simpl.con
cic:/Coq/Reals/RIneq/Rinv_neq_0_compat.con
cic:/Coq/Reals/RIneq/Rinv_r.con
cic:/Coq/Reals/RIneq/Rinv_r_simpl_l.con
cic:/Coq/Reals/RIneq/Rinv_r_simpl_m.con
cic:/Coq/Reals/RIneq/Rinv_r_simpl_r.con
cic:/Coq/Reals/RIneq/Rinv_r_sym.con
cic:/Coq/Reals/RIneq/Rle_0_1.con
cic:/Coq/Reals/RIneq/Rle_0_sqr.con
cic:/Coq/Reals/RIneq/Rle_antisym.con
cic:/Coq/Reals/RIneq/Rle_dec.con
cic:/Coq/Reals/RIneq/Rle_ge.con
cic:/Coq/Reals/RIneq/Rle_le_eq.con
cic:/Coq/Reals/RIneq/Rle_lt_0_plus_1.con
cic:/Coq/Reals/RIneq/Rle_lt_or_eq_dec.con
cic:/Coq/Reals/RIneq/Rle_lt_trans.con
cic:/Coq/Reals/RIneq/Rle_minus.con
cic:/Coq/Reals/RIneq/Rle_not_lt.con
cic:/Coq/Reals/RIneq/Rle_or_lt.con
cic:/Coq/Reals/RIneq/Rle_refl.con
cic:/Coq/Reals/RIneq/Rle_trans.con
cic:/Coq/Reals/RIneq/Rlt_0_1.con
cic:/Coq/Reals/RIneq/Rlt_0_sqr.con
cic:/Coq/Reals/RIneq/Rlt_dec.con
cic:/Coq/Reals/RIneq/Rlt_dichotomy_converse.con
cic:/Coq/Reals/RIneq/Rlt_eq_compat.con
cic:/Coq/Reals/RIneq/Rlt_irrefl.con
cic:/Coq/Reals/RIneq/Rlt_le.con
cic:/Coq/Reals/RIneq/Rlt_le_dec.con
cic:/Coq/Reals/RIneq/Rlt_le_trans.con
cic:/Coq/Reals/RIneq/Rlt_minus.con
cic:/Coq/Reals/RIneq/Rlt_not_eq.con
cic:/Coq/Reals/RIneq/Rlt_not_ge.con
cic:/Coq/Reals/RIneq/Rlt_not_le.con
cic:/Coq/Reals/RIneq/Rlt_plus_1.con
cic:/Coq/Reals/RIneq/Rminus_0_l.con
cic:/Coq/Reals/RIneq/Rminus_0_r.con
cic:/Coq/Reals/RIneq/Rminus_diag_eq.con
cic:/Coq/Reals/RIneq/Rminus_diag_uniq.con
cic:/Coq/Reals/RIneq/Rminus_diag_uniq_sym.con
cic:/Coq/Reals/RIneq/Rminus_eq_contra.con
cic:/Coq/Reals/RIneq/Rminus_le.con
cic:/Coq/Reals/RIneq/Rminus_lt.con
cic:/Coq/Reals/RIneq/Rminus_not_eq.con
cic:/Coq/Reals/RIneq/Rminus_not_eq_right.con
cic:/Coq/Reals/RIneq/Rmult_0_l.con
cic:/Coq/Reals/RIneq/Rmult_0_r.con
cic:/Coq/Reals/RIneq/Rmult_1_r.con
cic:/Coq/Reals/RIneq/Rmult_eq_0_compat.con
cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_l.con
cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_r.con
cic:/Coq/Reals/RIneq/Rmult_eq_compat_l.con
cic:/Coq/Reals/RIneq/Rmult_eq_reg_l.con
cic:/Coq/Reals/RIneq/Rmult_ge_0_gt_0_lt_compat.con
cic:/Coq/Reals/RIneq/Rmult_ge_compat_r.con
cic:/Coq/Reals/RIneq/Rmult_gt_0_compat.con
cic:/Coq/Reals/RIneq/Rmult_gt_0_lt_compat.con
cic:/Coq/Reals/RIneq/Rmult_integral.con
cic:/Coq/Reals/RIneq/Rmult_integral_contrapositive.con
cic:/Coq/Reals/RIneq/Rmult_le_0_lt_compat.con
cic:/Coq/Reals/RIneq/Rmult_le_compat.con
cic:/Coq/Reals/RIneq/Rmult_le_compat_l.con
cic:/Coq/Reals/RIneq/Rmult_le_compat_neg_l.con
cic:/Coq/Reals/RIneq/Rmult_le_compat_r.con
cic:/Coq/Reals/RIneq/Rmult_le_ge_compat_neg_l.con
cic:/Coq/Reals/RIneq/Rmult_le_pos.con
cic:/Coq/Reals/RIneq/Rmult_le_reg_l.con
cic:/Coq/Reals/RIneq/Rmult_lt_0_compat.con
cic:/Coq/Reals/RIneq/Rmult_lt_compat_r.con
cic:/Coq/Reals/RIneq/Rmult_lt_gt_compat_neg_l.con
cic:/Coq/Reals/RIneq/Rmult_lt_reg_l.con
cic:/Coq/Reals/RIneq/Rmult_minus_distr_l.con
cic:/Coq/Reals/RIneq/Rmult_ne.con
cic:/Coq/Reals/RIneq/Rmult_neq_0_reg.con
cic:/Coq/Reals/RIneq/Rmult_opp_opp.con
cic:/Coq/Reals/RIneq/Rmult_plus_distr_r.con
cic:/Coq/Reals/RIneq/Rnot_ge_lt.con
cic:/Coq/Reals/RIneq/Rnot_gt_le.con
cic:/Coq/Reals/RIneq/Rnot_le_lt.con
cic:/Coq/Reals/RIneq/Rnot_lt_ge.con
cic:/Coq/Reals/RIneq/Rnot_lt_le.con
cic:/Coq/Reals/RIneq/Ropp_0.con
cic:/Coq/Reals/RIneq/Ropp_0_ge_le_contravar.con
cic:/Coq/Reals/RIneq/Ropp_0_gt_lt_contravar.con
cic:/Coq/Reals/RIneq/Ropp_0_le_ge_contravar.con
cic:/Coq/Reals/RIneq/Ropp_0_lt_gt_contravar.con
cic:/Coq/Reals/RIneq/Ropp_Ropp_IZR.con
cic:/Coq/Reals/RIneq/Ropp_eq_0_compat.con
cic:/Coq/Reals/RIneq/Ropp_eq_compat.con
cic:/Coq/Reals/RIneq/Ropp_ge_le_contravar.con
cic:/Coq/Reals/RIneq/Ropp_gt_lt_0_contravar.con
cic:/Coq/Reals/RIneq/Ropp_gt_lt_contravar.con
cic:/Coq/Reals/RIneq/Ropp_inv_permute.con
cic:/Coq/Reals/RIneq/Ropp_involutive.con
cic:/Coq/Reals/RIneq/Ropp_le_cancel.con
cic:/Coq/Reals/RIneq/Ropp_le_contravar.con
cic:/Coq/Reals/RIneq/Ropp_le_ge_contravar.con
cic:/Coq/Reals/RIneq/Ropp_lt_cancel.con
cic:/Coq/Reals/RIneq/Ropp_lt_contravar.con
cic:/Coq/Reals/RIneq/Ropp_lt_gt_0_contravar.con
cic:/Coq/Reals/RIneq/Ropp_lt_gt_contravar.con
cic:/Coq/Reals/RIneq/Ropp_minus_distr'.con
cic:/Coq/Reals/RIneq/Ropp_minus_distr.con
cic:/Coq/Reals/RIneq/Ropp_mult_distr_l_reverse.con
cic:/Coq/Reals/RIneq/Ropp_mult_distr_r_reverse.con
cic:/Coq/Reals/RIneq/Ropp_neq_0_compat.con
cic:/Coq/Reals/RIneq/Ropp_plus_distr.con
cic:/Coq/Reals/RIneq/Rplus_0_r.con
cic:/Coq/Reals/RIneq/Rplus_0_r_uniq.con
cic:/Coq/Reals/RIneq/Rplus_eq_0_l.con
cic:/Coq/Reals/RIneq/Rplus_eq_R0.con
cic:/Coq/Reals/RIneq/Rplus_eq_compat_l.con
cic:/Coq/Reals/RIneq/Rplus_eq_reg_l.con
cic:/Coq/Reals/RIneq/Rplus_ge_compat_l.con
cic:/Coq/Reals/RIneq/Rplus_ge_reg_l.con
cic:/Coq/Reals/RIneq/Rplus_gt_compat_l.con
cic:/Coq/Reals/RIneq/Rplus_gt_reg_l.con
cic:/Coq/Reals/RIneq/Rplus_le_compat.con
cic:/Coq/Reals/RIneq/Rplus_le_compat_l.con
cic:/Coq/Reals/RIneq/Rplus_le_compat_r.con
cic:/Coq/Reals/RIneq/Rplus_le_le_0_compat.con
cic:/Coq/Reals/RIneq/Rplus_le_lt_0_compat.con
cic:/Coq/Reals/RIneq/Rplus_le_lt_compat.con
cic:/Coq/Reals/RIneq/Rplus_le_reg_l.con
cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con
cic:/Coq/Reals/RIneq/Rplus_lt_compat.con
cic:/Coq/Reals/RIneq/Rplus_lt_compat_r.con
cic:/Coq/Reals/RIneq/Rplus_lt_le_0_compat.con
cic:/Coq/Reals/RIneq/Rplus_lt_le_compat.con
cic:/Coq/Reals/RIneq/Rplus_lt_reg_r.con
cic:/Coq/Reals/RIneq/Rplus_minus.con
cic:/Coq/Reals/RIneq/Rplus_ne.con
cic:/Coq/Reals/RIneq/Rplus_opp_l.con
cic:/Coq/Reals/RIneq/Rplus_opp_r_uniq.con
cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0.con
cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0_l.con
cic:/Coq/Reals/RIneq/Rsqr.con
cic:/Coq/Reals/RIneq/Rsqr_0.con
cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con
cic:/Coq/Reals/RIneq/Rtotal_order.con
cic:/Coq/Reals/RIneq/S_INR.con
cic:/Coq/Reals/RIneq/S_O_plus_INR.con
cic:/Coq/Reals/RIneq/Z_R_minus.con
cic:/Coq/Reals/RIneq/completeness_weak.con
cic:/Coq/Reals/RIneq/cond_neg.con
cic:/Coq/Reals/RIneq/cond_nonneg.con
cic:/Coq/Reals/RIneq/cond_nonpos.con
cic:/Coq/Reals/RIneq/cond_nonzero.con
cic:/Coq/Reals/RIneq/cond_pos.con
cic:/Coq/Reals/RIneq/double.con
cic:/Coq/Reals/RIneq/double_var.con
cic:/Coq/Reals/RIneq/eq_IZR.con
cic:/Coq/Reals/RIneq/eq_IZR_R0.con
cic:/Coq/Reals/RIneq/inser_trans_R.con
cic:/Coq/Reals/RIneq/le_INR.con
cic:/Coq/Reals/RIneq/le_IZR.con
cic:/Coq/Reals/RIneq/le_IZR_R1.con
cic:/Coq/Reals/RIneq/le_O_IZR.con
cic:/Coq/Reals/RIneq/le_epsilon.con
cic:/Coq/Reals/RIneq/lt_INR.con
cic:/Coq/Reals/RIneq/lt_INR_0.con
cic:/Coq/Reals/RIneq/lt_IZR.con
cic:/Coq/Reals/RIneq/lt_O_IZR.con
cic:/Coq/Reals/RIneq/minus_INR.con
cic:/Coq/Reals/RIneq/minus_Rge.con
cic:/Coq/Reals/RIneq/minus_Rgt.con
cic:/Coq/Reals/RIneq/mult_INR.con
cic:/Coq/Reals/RIneq/mult_IZR.con
cic:/Coq/Reals/RIneq/neg.con
cic:/Coq/Reals/RIneq/negreal_ind.con
cic:/Coq/Reals/RIneq/negreal_rec.con
cic:/Coq/Reals/RIneq/negreal_rect.con
cic:/Coq/Reals/RIneq/nonneg.con
cic:/Coq/Reals/RIneq/nonnegreal_ind.con
cic:/Coq/Reals/RIneq/nonnegreal_rec.con
cic:/Coq/Reals/RIneq/nonnegreal_rect.con
cic:/Coq/Reals/RIneq/nonpos.con
cic:/Coq/Reals/RIneq/nonposreal_ind.con
cic:/Coq/Reals/RIneq/nonposreal_rec.con
cic:/Coq/Reals/RIneq/nonposreal_rect.con
cic:/Coq/Reals/RIneq/nonzero.con
cic:/Coq/Reals/RIneq/nonzeroreal_ind.con
cic:/Coq/Reals/RIneq/nonzeroreal_rec.con
cic:/Coq/Reals/RIneq/nonzeroreal_rect.con
cic:/Coq/Reals/RIneq/not_1_INR.con
cic:/Coq/Reals/RIneq/not_INR_O.con
cic:/Coq/Reals/RIneq/not_O_INR.con
cic:/Coq/Reals/RIneq/not_O_IZR.con
cic:/Coq/Reals/RIneq/not_nm_INR.con
cic:/Coq/Reals/RIneq/one_IZR_lt1.con
cic:/Coq/Reals/RIneq/one_IZR_r_R1.con
cic:/Coq/Reals/RIneq/one_IZR_r_R1_subproof.con
cic:/Coq/Reals/RIneq/plus_INR.con
cic:/Coq/Reals/RIneq/plus_IZR.con
cic:/Coq/Reals/RIneq/plus_IZR_NEG_POS.con
cic:/Coq/Reals/RIneq/plus_le_is_le.con
cic:/Coq/Reals/RIneq/plus_lt_is_lt.con
cic:/Coq/Reals/RIneq/pos.con
cic:/Coq/Reals/RIneq/pos_INR.con
cic:/Coq/Reals/RIneq/posreal_ind.con
cic:/Coq/Reals/RIneq/posreal_rec.con
cic:/Coq/Reals/RIneq/posreal_rect.con
cic:/Coq/Reals/RIneq/prod_neq_R0.con
cic:/Coq/Reals/RIneq/single_z_r_R1.con
cic:/Coq/Reals/RIneq/sum_inequa_Rle_lt.con
cic:/Coq/Reals/RIneq/tech_Rgt_minus.con
cic:/Coq/Reals/RIneq/tech_Rplus.con
cic:/Coq/Reals/RIneq/tech_single_z_r_R1.con
cic:/Coq/Reals/RList/AbsList.con
cic:/Coq/Reals/RList/AbsList_P1.con
cic:/Coq/Reals/RList/AbsList_P2.con
cic:/Coq/Reals/RList/FF.con
cic:/Coq/Reals/RList/In.con
cic:/Coq/Reals/RList/MaxRlist.con
cic:/Coq/Reals/RList/MaxRlist_P1.con
cic:/Coq/Reals/RList/MaxRlist_P2.con
cic:/Coq/Reals/RList/MinRlist.con
cic:/Coq/Reals/RList/MinRlist_P1.con
cic:/Coq/Reals/RList/MinRlist_P2.con
cic:/Coq/Reals/RList/RList_P0.con
cic:/Coq/Reals/RList/RList_P1.con
cic:/Coq/Reals/RList/RList_P10.con
cic:/Coq/Reals/RList/RList_P11.con
cic:/Coq/Reals/RList/RList_P12.con
cic:/Coq/Reals/RList/RList_P13.con
cic:/Coq/Reals/RList/RList_P14.con
cic:/Coq/Reals/RList/RList_P15.con
cic:/Coq/Reals/RList/RList_P16.con
cic:/Coq/Reals/RList/RList_P17.con
cic:/Coq/Reals/RList/RList_P18.con
cic:/Coq/Reals/RList/RList_P19.con
cic:/Coq/Reals/RList/RList_P2.con
cic:/Coq/Reals/RList/RList_P20.con
cic:/Coq/Reals/RList/RList_P21.con
cic:/Coq/Reals/RList/RList_P22.con
cic:/Coq/Reals/RList/RList_P23.con
cic:/Coq/Reals/RList/RList_P24.con
cic:/Coq/Reals/RList/RList_P25.con
cic:/Coq/Reals/RList/RList_P26.con
cic:/Coq/Reals/RList/RList_P27.con
cic:/Coq/Reals/RList/RList_P28.con
cic:/Coq/Reals/RList/RList_P29.con
cic:/Coq/Reals/RList/RList_P3.con
cic:/Coq/Reals/RList/RList_P4.con
cic:/Coq/Reals/RList/RList_P5.con
cic:/Coq/Reals/RList/RList_P6.con
cic:/Coq/Reals/RList/RList_P7.con
cic:/Coq/Reals/RList/RList_P8.con
cic:/Coq/Reals/RList/RList_P9.con
cic:/Coq/Reals/RList/Rlength.con
cic:/Coq/Reals/RList/Rlist_P1.con
cic:/Coq/Reals/RList/Rlist_ind.con
cic:/Coq/Reals/RList/Rlist_rec.con
cic:/Coq/Reals/RList/Rlist_rect.con
cic:/Coq/Reals/RList/Rtail.con
cic:/Coq/Reals/RList/app_Rlist.con
cic:/Coq/Reals/RList/cons_ORlist.con
cic:/Coq/Reals/RList/cons_Rlist.con
cic:/Coq/Reals/RList/insert.con
cic:/Coq/Reals/RList/mid_Rlist.con
cic:/Coq/Reals/RList/ordered_Rlist.con
cic:/Coq/Reals/RList/pos_Rl.con
cic:/Coq/Reals/RList/pos_Rl_P1.con
cic:/Coq/Reals/RList/pos_Rl_P2.con
cic:/Coq/Reals/R_Ifp/Int_part.con
cic:/Coq/Reals/R_Ifp/Int_part_INR.con
cic:/Coq/Reals/R_Ifp/R0_fp_O.con
cic:/Coq/Reals/R_Ifp/Rminus_Int_part1.con
cic:/Coq/Reals/R_Ifp/Rminus_Int_part2.con
cic:/Coq/Reals/R_Ifp/Rminus_fp1.con
cic:/Coq/Reals/R_Ifp/Rminus_fp2.con
cic:/Coq/Reals/R_Ifp/base_Int_part.con
cic:/Coq/Reals/R_Ifp/base_fp.con
cic:/Coq/Reals/R_Ifp/for_base_fp.con
cic:/Coq/Reals/R_Ifp/fp_R0.con
cic:/Coq/Reals/R_Ifp/fp_nat.con
cic:/Coq/Reals/R_Ifp/frac_part.con
cic:/Coq/Reals/R_Ifp/plus_Int_part1.con
cic:/Coq/Reals/R_Ifp/plus_Int_part2.con
cic:/Coq/Reals/R_Ifp/plus_frac_part1.con
cic:/Coq/Reals/R_Ifp/plus_frac_part2.con
cic:/Coq/Reals/R_Ifp/tech_up.con
cic:/Coq/Reals/R_Ifp/up_tech.con
cic:/Coq/Reals/R_sqr/Rsqr_1.con
cic:/Coq/Reals/R_sqr/Rsqr_abs.con
cic:/Coq/Reals/R_sqr/Rsqr_div.con
cic:/Coq/Reals/R_sqr/Rsqr_eq.con
cic:/Coq/Reals/R_sqr/Rsqr_eq_0.con
cic:/Coq/Reals/R_sqr/Rsqr_eq_abs_0.con
cic:/Coq/Reals/R_sqr/Rsqr_eq_asb_1.con
cic:/Coq/Reals/R_sqr/Rsqr_gt_0_0.con
cic:/Coq/Reals/R_sqr/Rsqr_incr_0.con
cic:/Coq/Reals/R_sqr/Rsqr_incr_0_var.con
cic:/Coq/Reals/R_sqr/Rsqr_incr_1.con
cic:/Coq/Reals/R_sqr/Rsqr_incrst_0.con
cic:/Coq/Reals/R_sqr/Rsqr_incrst_1.con
cic:/Coq/Reals/R_sqr/Rsqr_inj.con
cic:/Coq/Reals/R_sqr/Rsqr_inv.con
cic:/Coq/Reals/R_sqr/Rsqr_le_abs_0.con
cic:/Coq/Reals/R_sqr/Rsqr_le_abs_1.con
cic:/Coq/Reals/R_sqr/Rsqr_lt_abs_0.con
cic:/Coq/Reals/R_sqr/Rsqr_lt_abs_1.con
cic:/Coq/Reals/R_sqr/Rsqr_minus.con
cic:/Coq/Reals/R_sqr/Rsqr_minus_plus.con
cic:/Coq/Reals/R_sqr/Rsqr_mult.con
cic:/Coq/Reals/R_sqr/Rsqr_neg.con
cic:/Coq/Reals/R_sqr/Rsqr_neg_minus.con
cic:/Coq/Reals/R_sqr/Rsqr_neg_pos_le_0.con
cic:/Coq/Reals/R_sqr/Rsqr_neg_pos_le_1.con
cic:/Coq/Reals/R_sqr/Rsqr_plus.con
cic:/Coq/Reals/R_sqr/Rsqr_plus_minus.con
cic:/Coq/Reals/R_sqr/Rsqr_pos_lt.con
cic:/Coq/Reals/R_sqr/canonical_Rsqr.con
cic:/Coq/Reals/R_sqr/neg_pos_Rsqr_le.con
cic:/Coq/Reals/R_sqr/triangle_rectangle.con
cic:/Coq/Reals/R_sqr/triangle_rectangle_le.con
cic:/Coq/Reals/R_sqr/triangle_rectangle_lt.con
cic:/Coq/Reals/R_sqrt/Delta.con
cic:/Coq/Reals/R_sqrt/Delta_is_pos.con
cic:/Coq/Reals/R_sqrt/Rsqr_sol_eq_0_0.con
cic:/Coq/Reals/R_sqrt/Rsqr_sol_eq_0_1.con
cic:/Coq/Reals/R_sqrt/Rsqr_sqrt.con
cic:/Coq/Reals/R_sqrt/sol_x1.con
cic:/Coq/Reals/R_sqrt/sol_x2.con
cic:/Coq/Reals/R_sqrt/sqrt.con
cic:/Coq/Reals/R_sqrt/sqrt_0.con
cic:/Coq/Reals/R_sqrt/sqrt_1.con
cic:/Coq/Reals/R_sqrt/sqrt_Rsqr.con
cic:/Coq/Reals/R_sqrt/sqrt_Rsqr_abs.con
cic:/Coq/Reals/R_sqrt/sqrt_cauchy.con
cic:/Coq/Reals/R_sqrt/sqrt_def.con
cic:/Coq/Reals/R_sqrt/sqrt_div.con
cic:/Coq/Reals/R_sqrt/sqrt_eq_0.con
cic:/Coq/Reals/R_sqrt/sqrt_inj.con
cic:/Coq/Reals/R_sqrt/sqrt_le_0.con
cic:/Coq/Reals/R_sqrt/sqrt_le_1.con
cic:/Coq/Reals/R_sqrt/sqrt_lem_0.con
cic:/Coq/Reals/R_sqrt/sqrt_less.con
cic:/Coq/Reals/R_sqrt/sqrt_lt_0.con
cic:/Coq/Reals/R_sqrt/sqrt_lt_1.con
cic:/Coq/Reals/R_sqrt/sqrt_lt_R0.con
cic:/Coq/Reals/R_sqrt/sqrt_more.con
cic:/Coq/Reals/R_sqrt/sqrt_mult.con
cic:/Coq/Reals/R_sqrt/sqrt_positivity.con
cic:/Coq/Reals/R_sqrt/sqrt_sqrt.con
cic:/Coq/Reals/R_sqrt/sqrt_square.con
cic:/Coq/Reals/R_sqrt/sqtr_lem_1.con
cic:/Coq/Reals/Raxioms/INR.con
cic:/Coq/Reals/Raxioms/IZR.con
cic:/Coq/Reals/Raxioms/R1_neq_R0.con
cic:/Coq/Reals/Raxioms/Rinv_l.con
cic:/Coq/Reals/Raxioms/Rlt_asym.con
cic:/Coq/Reals/Raxioms/Rlt_trans.con
cic:/Coq/Reals/Raxioms/Rmult_1_l.con
cic:/Coq/Reals/Raxioms/Rmult_assoc.con
cic:/Coq/Reals/Raxioms/Rmult_comm.con
cic:/Coq/Reals/Raxioms/Rmult_lt_compat_l.con
cic:/Coq/Reals/Raxioms/Rmult_plus_distr_l.con
cic:/Coq/Reals/Raxioms/Rplus_0_l.con
cic:/Coq/Reals/Raxioms/Rplus_assoc.con
cic:/Coq/Reals/Raxioms/Rplus_comm.con
cic:/Coq/Reals/Raxioms/Rplus_lt_compat_l.con
cic:/Coq/Reals/Raxioms/Rplus_opp_r.con
cic:/Coq/Reals/Raxioms/archimed.con
cic:/Coq/Reals/Raxioms/bound.con
cic:/Coq/Reals/Raxioms/completeness.con
cic:/Coq/Reals/Raxioms/is_lub.con
cic:/Coq/Reals/Raxioms/is_upper_bound.con
cic:/Coq/Reals/Raxioms/total_order_T.con
cic:/Coq/Reals/Rbasic_fun/RRle_abs.con
cic:/Coq/Reals/Rbasic_fun/RRle_abs_subproof.con
cic:/Coq/Reals/Rbasic_fun/RRle_abs_subproof0.con
cic:/Coq/Reals/Rbasic_fun/Rabs.con
cic:/Coq/Reals/Rbasic_fun/Rabs_R0.con
cic:/Coq/Reals/Rbasic_fun/Rabs_R1.con
cic:/Coq/Reals/Rbasic_fun/Rabs_Rabsolu.con
cic:/Coq/Reals/Rbasic_fun/Rabs_Rinv.con
cic:/Coq/Reals/Rbasic_fun/Rabs_Ropp.con
cic:/Coq/Reals/Rbasic_fun/Rabs_Zabs.con
cic:/Coq/Reals/Rbasic_fun/Rabs_def1.con
cic:/Coq/Reals/Rbasic_fun/Rabs_def2.con
cic:/Coq/Reals/Rbasic_fun/Rabs_left.con
cic:/Coq/Reals/Rbasic_fun/Rabs_left1.con
cic:/Coq/Reals/Rbasic_fun/Rabs_minus_sym.con
cic:/Coq/Reals/Rbasic_fun/Rabs_mult.con
cic:/Coq/Reals/Rbasic_fun/Rabs_no_R0.con
cic:/Coq/Reals/Rbasic_fun/Rabs_pos.con
cic:/Coq/Reals/Rbasic_fun/Rabs_pos_eq.con
cic:/Coq/Reals/Rbasic_fun/Rabs_pos_lt.con
cic:/Coq/Reals/Rbasic_fun/Rabs_right.con
cic:/Coq/Reals/Rbasic_fun/Rabs_triang.con
cic:/Coq/Reals/Rbasic_fun/Rabs_triang_inv.con
cic:/Coq/Reals/Rbasic_fun/Rabs_triang_inv2.con
cic:/Coq/Reals/Rbasic_fun/Rcase_abs.con
cic:/Coq/Reals/Rbasic_fun/Rmax.con
cic:/Coq/Reals/Rbasic_fun/RmaxAbs.con
cic:/Coq/Reals/Rbasic_fun/RmaxLess1.con
cic:/Coq/Reals/Rbasic_fun/RmaxLess2.con
cic:/Coq/Reals/Rbasic_fun/RmaxRmult.con
cic:/Coq/Reals/Rbasic_fun/RmaxSym.con
cic:/Coq/Reals/Rbasic_fun/Rmax_Rle.con
cic:/Coq/Reals/Rbasic_fun/Rmax_stable_in_negreal.con
cic:/Coq/Reals/Rbasic_fun/Rmin.con
cic:/Coq/Reals/Rbasic_fun/Rmin_Rgt.con
cic:/Coq/Reals/Rbasic_fun/Rmin_Rgt_l.con
cic:/Coq/Reals/Rbasic_fun/Rmin_Rgt_r.con
cic:/Coq/Reals/Rbasic_fun/Rmin_comm.con
cic:/Coq/Reals/Rbasic_fun/Rmin_l.con
cic:/Coq/Reals/Rbasic_fun/Rmin_r.con
cic:/Coq/Reals/Rbasic_fun/Rmin_stable_in_posreal.con
cic:/Coq/Reals/Rcomplete/R_complete.con
cic:/Coq/Reals/Rdefinitions/R.con
cic:/Coq/Reals/Rdefinitions/R0.con
cic:/Coq/Reals/Rdefinitions/R1.con
cic:/Coq/Reals/Rdefinitions/Rdiv.con
cic:/Coq/Reals/Rdefinitions/Rge.con
cic:/Coq/Reals/Rdefinitions/Rgt.con
cic:/Coq/Reals/Rdefinitions/Rinv.con
cic:/Coq/Reals/Rdefinitions/Rle.con
cic:/Coq/Reals/Rdefinitions/Rlt.con
cic:/Coq/Reals/Rdefinitions/Rminus.con
cic:/Coq/Reals/Rdefinitions/Rmult.con
cic:/Coq/Reals/Rdefinitions/Ropp.con
cic:/Coq/Reals/Rdefinitions/Rplus.con
cic:/Coq/Reals/Rdefinitions/up.con
cic:/Coq/Reals/Rderiv/D_in.con
cic:/Coq/Reals/Rderiv/D_pow_n.con
cic:/Coq/Reals/Rderiv/D_x.con
cic:/Coq/Reals/Rderiv/Dadd.con
cic:/Coq/Reals/Rderiv/Dcomp.con
cic:/Coq/Reals/Rderiv/Dconst.con
cic:/Coq/Reals/Rderiv/Dminus.con
cic:/Coq/Reals/Rderiv/Dmult.con
cic:/Coq/Reals/Rderiv/Dmult_const.con
cic:/Coq/Reals/Rderiv/Dopp.con
cic:/Coq/Reals/Rderiv/Dx.con
cic:/Coq/Reals/Rderiv/Dx_pow_n.con
cic:/Coq/Reals/Rderiv/cont_deriv.con
cic:/Coq/Reals/Rderiv/cont_deriv_subproof.con
cic:/Coq/Reals/Rderiv/cont_deriv_subproof0.con
cic:/Coq/Reals/Rderiv/continue_in.con
cic:/Coq/Reals/Rfunctions/GP_finite.con
cic:/Coq/Reals/Rfunctions/INR_fact_neq_0.con
cic:/Coq/Reals/Rfunctions/Pow_x_infinity.con
cic:/Coq/Reals/Rfunctions/Power_monotonic.con
cic:/Coq/Reals/Rfunctions/RPow_abs.con
cic:/Coq/Reals/Rfunctions/R_dist.con
cic:/Coq/Reals/Rfunctions/R_dist_eq.con
cic:/Coq/Reals/Rfunctions/R_dist_plus.con
cic:/Coq/Reals/Rfunctions/R_dist_pos.con
cic:/Coq/Reals/Rfunctions/R_dist_refl.con
cic:/Coq/Reals/Rfunctions/R_dist_sym.con
cic:/Coq/Reals/Rfunctions/R_dist_tri.con
cic:/Coq/Reals/Rfunctions/Rinv_pow.con
cic:/Coq/Reals/Rfunctions/Rle_pow.con
cic:/Coq/Reals/Rfunctions/Rlt_pow.con
cic:/Coq/Reals/Rfunctions/Rlt_pow_R1.con
cic:/Coq/Reals/Rfunctions/Zpower_NR0.con
cic:/Coq/Reals/Rfunctions/Zpower_nat_powerRZ.con
cic:/Coq/Reals/Rfunctions/Zpower_nat_powerRZ_absolu.con
cic:/Coq/Reals/Rfunctions/decimal_exp.con
cic:/Coq/Reals/Rfunctions/fact_simpl.con
cic:/Coq/Reals/Rfunctions/infinit_sum.con
cic:/Coq/Reals/Rfunctions/poly.con
cic:/Coq/Reals/Rfunctions/pow.con
cic:/Coq/Reals/Rfunctions/pow1.con
cic:/Coq/Reals/Rfunctions/pow_1.con
cic:/Coq/Reals/Rfunctions/pow_1_abs.con
cic:/Coq/Reals/Rfunctions/pow_1_even.con
cic:/Coq/Reals/Rfunctions/pow_1_odd.con
cic:/Coq/Reals/Rfunctions/pow_O.con
cic:/Coq/Reals/Rfunctions/pow_R1.con
cic:/Coq/Reals/Rfunctions/pow_R1_Rle.con
cic:/Coq/Reals/Rfunctions/pow_RN_plus.con
cic:/Coq/Reals/Rfunctions/pow_Rabs.con
cic:/Coq/Reals/Rfunctions/pow_Rsqr.con
cic:/Coq/Reals/Rfunctions/pow_add.con
cic:/Coq/Reals/Rfunctions/pow_incr.con
cic:/Coq/Reals/Rfunctions/pow_le.con
cic:/Coq/Reals/Rfunctions/pow_lt.con
cic:/Coq/Reals/Rfunctions/pow_lt_1_zero.con
cic:/Coq/Reals/Rfunctions/pow_maj_Rabs.con
cic:/Coq/Reals/Rfunctions/pow_mult.con
cic:/Coq/Reals/Rfunctions/pow_ne_zero.con
cic:/Coq/Reals/Rfunctions/pow_nonzero.con
cic:/Coq/Reals/Rfunctions/powerRZ.con
cic:/Coq/Reals/Rfunctions/powerRZ_1.con
cic:/Coq/Reals/Rfunctions/powerRZ_NOR.con
cic:/Coq/Reals/Rfunctions/powerRZ_O.con
cic:/Coq/Reals/Rfunctions/powerRZ_R1.con
cic:/Coq/Reals/Rfunctions/powerRZ_add.con
cic:/Coq/Reals/Rfunctions/powerRZ_le.con
cic:/Coq/Reals/Rfunctions/powerRZ_lt.con
cic:/Coq/Reals/Rfunctions/simpl_fact.con
cic:/Coq/Reals/Rfunctions/sum_f.con
cic:/Coq/Reals/Rfunctions/sum_f_R0.con
cic:/Coq/Reals/Rfunctions/sum_f_R0_triangle.con
cic:/Coq/Reals/Rfunctions/sum_nat.con
cic:/Coq/Reals/Rfunctions/sum_nat_O.con
cic:/Coq/Reals/Rfunctions/sum_nat_f.con
cic:/Coq/Reals/Rfunctions/sum_nat_f_O.con
cic:/Coq/Reals/Rfunctions/tech_pow_Rmult.con
cic:/Coq/Reals/Rfunctions/tech_pow_Rplus.con
cic:/Coq/Reals/Rlimit/Base.con
cic:/Coq/Reals/Rlimit/Dgf.con
cic:/Coq/Reals/Rlimit/Metric_Space_ind.con
cic:/Coq/Reals/Rlimit/Metric_Space_rec.con
cic:/Coq/Reals/Rlimit/Metric_Space_rect.con
cic:/Coq/Reals/Rlimit/R_met.con
cic:/Coq/Reals/Rlimit/Rlt_eps2_eps.con
cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con
cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof0.con
cic:/Coq/Reals/Rlimit/Rlt_eps4_eps.con
cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof.con
cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof0.con
cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof1.con
cic:/Coq/Reals/Rlimit/adhDa.con
cic:/Coq/Reals/Rlimit/dist.con
cic:/Coq/Reals/Rlimit/dist_pos.con
cic:/Coq/Reals/Rlimit/dist_refl.con
cic:/Coq/Reals/Rlimit/dist_sym.con
cic:/Coq/Reals/Rlimit/dist_tri.con
cic:/Coq/Reals/Rlimit/eps2.con
cic:/Coq/Reals/Rlimit/eps2_Rgt_R0.con
cic:/Coq/Reals/Rlimit/eps2_Rgt_R0_subproof.con
cic:/Coq/Reals/Rlimit/eps4.con
cic:/Coq/Reals/Rlimit/lim_x.con
cic:/Coq/Reals/Rlimit/limit1_in.con
cic:/Coq/Reals/Rlimit/limit_Ropp.con
cic:/Coq/Reals/Rlimit/limit_comp.con
cic:/Coq/Reals/Rlimit/limit_free.con
cic:/Coq/Reals/Rlimit/limit_in.con
cic:/Coq/Reals/Rlimit/limit_inv.con
cic:/Coq/Reals/Rlimit/limit_minus.con
cic:/Coq/Reals/Rlimit/limit_mul.con
cic:/Coq/Reals/Rlimit/limit_plus.con
cic:/Coq/Reals/Rlimit/mul_factor.con
cic:/Coq/Reals/Rlimit/mul_factor_gt.con
cic:/Coq/Reals/Rlimit/mul_factor_gt_f.con
cic:/Coq/Reals/Rlimit/mul_factor_wd.con
cic:/Coq/Reals/Rlimit/prop_eps.con
cic:/Coq/Reals/Rlimit/single_limit.con
cic:/Coq/Reals/Rlimit/tech_limit.con
cic:/Coq/Reals/Rlimit/tech_limit_contr.con
cic:/Coq/Reals/Rpower/D_in_ext.con
cic:/Coq/Reals/Rpower/D_in_imp.con
cic:/Coq/Reals/Rpower/P_Rmin.con
cic:/Coq/Reals/Rpower/Rinv_Rdiv.con
cic:/Coq/Reals/Rpower/Rle_Rpower.con
cic:/Coq/Reals/Rpower/Rln.con
cic:/Coq/Reals/Rpower/Rpower.con
cic:/Coq/Reals/Rpower/Rpower_1.con
cic:/Coq/Reals/Rpower/Rpower_O.con
cic:/Coq/Reals/Rpower/Rpower_Ropp.con
cic:/Coq/Reals/Rpower/Rpower_lt.con
cic:/Coq/Reals/Rpower/Rpower_plus.con
cic:/Coq/Reals/Rpower/derivable_pt_lim_ln.con
cic:/Coq/Reals/Rpower/exp_Ropp.con
cic:/Coq/Reals/Rpower/exp_increasing.con
cic:/Coq/Reals/Rpower/exp_ineq1.con
cic:/Coq/Reals/Rpower/exp_inv.con
cic:/Coq/Reals/Rpower/exp_le_3.con
cic:/Coq/Reals/Rpower/exp_ln.con
cic:/Coq/Reals/Rpower/exp_lt_inv.con
cic:/Coq/Reals/Rpower/limit1_ext.con
cic:/Coq/Reals/Rpower/limit1_imp.con
cic:/Coq/Reals/Rpower/ln.con
cic:/Coq/Reals/Rpower/ln_1.con
cic:/Coq/Reals/Rpower/ln_Rinv.con
cic:/Coq/Reals/Rpower/ln_continue.con
cic:/Coq/Reals/Rpower/ln_exists.con
cic:/Coq/Reals/Rpower/ln_exists1.con
cic:/Coq/Reals/Rpower/ln_exp.con
cic:/Coq/Reals/Rpower/ln_increasing.con
cic:/Coq/Reals/Rpower/ln_inv.con
cic:/Coq/Reals/Rpower/ln_lt_2.con
cic:/Coq/Reals/Rpower/ln_lt_inv.con
cic:/Coq/Reals/Rpower/ln_mult.con
cic:/Coq/Reals/Rprod/C_maj.con
cic:/Coq/Reals/Rprod/INR_fact_lt_0.con
cic:/Coq/Reals/Rprod/RfactN_fact2N_factk.con
cic:/Coq/Reals/Rprod/fact_prodSO.con
cic:/Coq/Reals/Rprod/le_n_2n.con
cic:/Coq/Reals/Rprod/prod_SO_Rle.con
cic:/Coq/Reals/Rprod/prod_SO_pos.con
cic:/Coq/Reals/Rprod/prod_SO_split.con
cic:/Coq/Reals/Rprod/prod_f_SO.con
cic:/Coq/Reals/Rseries/Cauchy_crit.con
cic:/Coq/Reals/Rseries/EUn.con
cic:/Coq/Reals/Rseries/EUn_noempty.con
cic:/Coq/Reals/Rseries/GP_infinite.con
cic:/Coq/Reals/Rseries/Pser.con
cic:/Coq/Reals/Rseries/Rmax_N.con
cic:/Coq/Reals/Rseries/Un_bound_imp.con
cic:/Coq/Reals/Rseries/Un_cv.con
cic:/Coq/Reals/Rseries/Un_cv_crit.con
cic:/Coq/Reals/Rseries/Un_growing.con
cic:/Coq/Reals/Rseries/Un_in_EUn.con
cic:/Coq/Reals/Rseries/cauchy_bound.con
cic:/Coq/Reals/Rseries/finite_greater.con
cic:/Coq/Reals/Rseries/growing_prop.con
cic:/Coq/Reals/Rsigma/sigma.con
cic:/Coq/Reals/Rsigma/sigma_diff.con
cic:/Coq/Reals/Rsigma/sigma_diff_neg.con
cic:/Coq/Reals/Rsigma/sigma_eq_arg.con
cic:/Coq/Reals/Rsigma/sigma_first.con
cic:/Coq/Reals/Rsigma/sigma_last.con
cic:/Coq/Reals/Rsigma/sigma_split.con
cic:/Coq/Reals/Rsqrt_def/Dichotomy_lb.con
cic:/Coq/Reals/Rsqrt_def/Dichotomy_ub.con
cic:/Coq/Reals/Rsqrt_def/IVT.con
cic:/Coq/Reals/Rsqrt_def/IVT_cor.con
cic:/Coq/Reals/Rsqrt_def/Rsqrt.con
cic:/Coq/Reals/Rsqrt_def/Rsqrt_Rsqrt.con
cic:/Coq/Reals/Rsqrt_def/Rsqrt_exists.con
cic:/Coq/Reals/Rsqrt_def/Rsqrt_positivity.con
cic:/Coq/Reals/Rsqrt_def/cond_positivity.con
cic:/Coq/Reals/Rsqrt_def/continuity_seq.con
cic:/Coq/Reals/Rsqrt_def/cv_dicho.con
cic:/Coq/Reals/Rsqrt_def/dicho_comp.con
cic:/Coq/Reals/Rsqrt_def/dicho_lb.con
cic:/Coq/Reals/Rsqrt_def/dicho_lb_car.con
cic:/Coq/Reals/Rsqrt_def/dicho_lb_cv.con
cic:/Coq/Reals/Rsqrt_def/dicho_lb_dicho_up.con
cic:/Coq/Reals/Rsqrt_def/dicho_lb_growing.con
cic:/Coq/Reals/Rsqrt_def/dicho_lb_maj.con
cic:/Coq/Reals/Rsqrt_def/dicho_lb_maj_y.con
cic:/Coq/Reals/Rsqrt_def/dicho_up.con
cic:/Coq/Reals/Rsqrt_def/dicho_up_car.con
cic:/Coq/Reals/Rsqrt_def/dicho_up_cv.con
cic:/Coq/Reals/Rsqrt_def/dicho_up_decreasing.con
cic:/Coq/Reals/Rsqrt_def/dicho_up_min.con
cic:/Coq/Reals/Rsqrt_def/dicho_up_min_x.con
cic:/Coq/Reals/Rsqrt_def/pow_2_n.con
cic:/Coq/Reals/Rsqrt_def/pow_2_n_growing.con
cic:/Coq/Reals/Rsqrt_def/pow_2_n_infty.con
cic:/Coq/Reals/Rsqrt_def/pow_2_n_neq_R0.con
cic:/Coq/Reals/Rtopology/Bolzano_Weierstrass.con
cic:/Coq/Reals/Rtopology/Heine.con
cic:/Coq/Reals/Rtopology/Rlt_Rminus.con
cic:/Coq/Reals/Rtopology/Rsepare.con
cic:/Coq/Reals/Rtopology/ValAdh.con
cic:/Coq/Reals/Rtopology/ValAdh_un.con
cic:/Coq/Reals/Rtopology/ValAdh_un_exists.con
cic:/Coq/Reals/Rtopology/ValAdh_un_prop.con
cic:/Coq/Reals/Rtopology/adherence.con
cic:/Coq/Reals/Rtopology/adherence_P1.con
cic:/Coq/Reals/Rtopology/adherence_P2.con
cic:/Coq/Reals/Rtopology/adherence_P3.con
cic:/Coq/Reals/Rtopology/adherence_P4.con
cic:/Coq/Reals/Rtopology/bounded.con
cic:/Coq/Reals/Rtopology/closed_set.con
cic:/Coq/Reals/Rtopology/closed_set_P1.con
cic:/Coq/Reals/Rtopology/compact.con
cic:/Coq/Reals/Rtopology/compact_EMP.con
cic:/Coq/Reals/Rtopology/compact_P1.con
cic:/Coq/Reals/Rtopology/compact_P2.con
cic:/Coq/Reals/Rtopology/compact_P3.con
cic:/Coq/Reals/Rtopology/compact_P4.con
cic:/Coq/Reals/Rtopology/compact_P5.con
cic:/Coq/Reals/Rtopology/compact_P6.con
cic:/Coq/Reals/Rtopology/compact_carac.con
cic:/Coq/Reals/Rtopology/compact_eqDom.con
cic:/Coq/Reals/Rtopology/complementary.con
cic:/Coq/Reals/Rtopology/complementary_P1.con
cic:/Coq/Reals/Rtopology/cond_fam.con
cic:/Coq/Reals/Rtopology/continuity_P1.con
cic:/Coq/Reals/Rtopology/continuity_P2.con
cic:/Coq/Reals/Rtopology/continuity_P3.con
cic:/Coq/Reals/Rtopology/continuity_ab_maj.con
cic:/Coq/Reals/Rtopology/continuity_ab_min.con
cic:/Coq/Reals/Rtopology/continuity_compact.con
cic:/Coq/Reals/Rtopology/covering.con
cic:/Coq/Reals/Rtopology/covering_finite.con
cic:/Coq/Reals/Rtopology/covering_open_set.con
cic:/Coq/Reals/Rtopology/disc.con
cic:/Coq/Reals/Rtopology/disc_P1.con
cic:/Coq/Reals/Rtopology/domain_P1.con
cic:/Coq/Reals/Rtopology/domain_finite.con
cic:/Coq/Reals/Rtopology/eq_Dom.con
cic:/Coq/Reals/Rtopology/f.con
cic:/Coq/Reals/Rtopology/family_P1.con
cic:/Coq/Reals/Rtopology/family_closed_set.con
cic:/Coq/Reals/Rtopology/family_finite.con
cic:/Coq/Reals/Rtopology/family_ind.con
cic:/Coq/Reals/Rtopology/family_open_set.con
cic:/Coq/Reals/Rtopology/family_rec.con
cic:/Coq/Reals/Rtopology/family_rect.con
cic:/Coq/Reals/Rtopology/image_dir.con
cic:/Coq/Reals/Rtopology/image_rec.con
cic:/Coq/Reals/Rtopology/included.con
cic:/Coq/Reals/Rtopology/included_trans.con
cic:/Coq/Reals/Rtopology/ind.con
cic:/Coq/Reals/Rtopology/interior.con
cic:/Coq/Reals/Rtopology/interior_P1.con
cic:/Coq/Reals/Rtopology/interior_P2.con
cic:/Coq/Reals/Rtopology/interior_P3.con
cic:/Coq/Reals/Rtopology/intersection_domain.con
cic:/Coq/Reals/Rtopology/intersection_family.con
cic:/Coq/Reals/Rtopology/intersection_vide_finite_in.con
cic:/Coq/Reals/Rtopology/intersection_vide_in.con
cic:/Coq/Reals/Rtopology/is_lub_u.con
cic:/Coq/Reals/Rtopology/neighbourhood.con
cic:/Coq/Reals/Rtopology/neighbourhood_P1.con
cic:/Coq/Reals/Rtopology/open_set.con
cic:/Coq/Reals/Rtopology/open_set_P1.con
cic:/Coq/Reals/Rtopology/open_set_P2.con
cic:/Coq/Reals/Rtopology/open_set_P3.con
cic:/Coq/Reals/Rtopology/open_set_P4.con
cic:/Coq/Reals/Rtopology/open_set_P5.con
cic:/Coq/Reals/Rtopology/open_set_P6.con
cic:/Coq/Reals/Rtopology/point_adherent.con
cic:/Coq/Reals/Rtopology/prolongement_C0.con
cic:/Coq/Reals/Rtopology/restriction_family.con
cic:/Coq/Reals/Rtopology/subfamily.con
cic:/Coq/Reals/Rtopology/uniform_continuity.con
cic:/Coq/Reals/Rtopology/union_domain.con
cic:/Coq/Reals/Rtrigo/COS.con
cic:/Coq/Reals/Rtrigo/COS_bound.con
cic:/Coq/Reals/Rtrigo/PI2_RGT_0.con
cic:/Coq/Reals/Rtrigo/PI2_Rlt_PI.con
cic:/Coq/Reals/Rtrigo/PI4_RLT_PI2.con
cic:/Coq/Reals/Rtrigo/PI_neq0.con
cic:/Coq/Reals/Rtrigo/SIN.con
cic:/Coq/Reals/Rtrigo/SIN_bound.con
cic:/Coq/Reals/Rtrigo/_PI2_RLT_0.con
cic:/Coq/Reals/Rtrigo/cos2.con
cic:/Coq/Reals/Rtrigo/cos_2PI.con
cic:/Coq/Reals/Rtrigo/cos_2a.con
cic:/Coq/Reals/Rtrigo/cos_2a_cos.con
cic:/Coq/Reals/Rtrigo/cos_2a_sin.con
cic:/Coq/Reals/Rtrigo/cos_3PI2.con
cic:/Coq/Reals/Rtrigo/cos_PI.con
cic:/Coq/Reals/Rtrigo/cos_PI2.con
cic:/Coq/Reals/Rtrigo/cos_decr_0.con
cic:/Coq/Reals/Rtrigo/cos_decr_1.con
cic:/Coq/Reals/Rtrigo/cos_decreasing_0.con
cic:/Coq/Reals/Rtrigo/cos_decreasing_1.con
cic:/Coq/Reals/Rtrigo/cos_eq_0_1.con
cic:/Coq/Reals/Rtrigo/cos_eq_0_2PI_0.con
cic:/Coq/Reals/Rtrigo/cos_eq_0_2PI_1.con
cic:/Coq/Reals/Rtrigo/cos_ge_0.con
cic:/Coq/Reals/Rtrigo/cos_gt_0.con
cic:/Coq/Reals/Rtrigo/cos_incr_0.con
cic:/Coq/Reals/Rtrigo/cos_incr_1.con
cic:/Coq/Reals/Rtrigo/cos_increasing_0.con
cic:/Coq/Reals/Rtrigo/cos_increasing_1.con
cic:/Coq/Reals/Rtrigo/cos_lb.con
cic:/Coq/Reals/Rtrigo/cos_le_0.con
cic:/Coq/Reals/Rtrigo/cos_lt_0.con
cic:/Coq/Reals/Rtrigo/cos_minus.con
cic:/Coq/Reals/Rtrigo/cos_neg.con
cic:/Coq/Reals/Rtrigo/cos_period.con
cic:/Coq/Reals/Rtrigo/cos_shift.con
cic:/Coq/Reals/Rtrigo/cos_sin.con
cic:/Coq/Reals/Rtrigo/cos_sin_0.con
cic:/Coq/Reals/Rtrigo/cos_sin_0_var.con
cic:/Coq/Reals/Rtrigo/cos_ub.con
cic:/Coq/Reals/Rtrigo/form1.con
cic:/Coq/Reals/Rtrigo/form2.con
cic:/Coq/Reals/Rtrigo/form3.con
cic:/Coq/Reals/Rtrigo/form4.con
cic:/Coq/Reals/Rtrigo/neg_cos.con
cic:/Coq/Reals/Rtrigo/neg_sin.con
cic:/Coq/Reals/Rtrigo/sin2.con
cic:/Coq/Reals/Rtrigo/sin2_cos2.con
cic:/Coq/Reals/Rtrigo/sin_2PI.con
cic:/Coq/Reals/Rtrigo/sin_2a.con
cic:/Coq/Reals/Rtrigo/sin_PI.con
cic:/Coq/Reals/Rtrigo/sin_PI2.con
cic:/Coq/Reals/Rtrigo/sin_PI_x.con
cic:/Coq/Reals/Rtrigo/sin_cos.con
cic:/Coq/Reals/Rtrigo/sin_decr_0.con
cic:/Coq/Reals/Rtrigo/sin_decr_1.con
cic:/Coq/Reals/Rtrigo/sin_decreasing_0.con
cic:/Coq/Reals/Rtrigo/sin_decreasing_1.con
cic:/Coq/Reals/Rtrigo/sin_eq_0_0.con
cic:/Coq/Reals/Rtrigo/sin_eq_0_1.con
cic:/Coq/Reals/Rtrigo/sin_eq_O_2PI_0.con
cic:/Coq/Reals/Rtrigo/sin_eq_O_2PI_1.con
cic:/Coq/Reals/Rtrigo/sin_ge_0.con
cic:/Coq/Reals/Rtrigo/sin_gt_0.con
cic:/Coq/Reals/Rtrigo/sin_incr_0.con
cic:/Coq/Reals/Rtrigo/sin_incr_1.con
cic:/Coq/Reals/Rtrigo/sin_increasing_0.con
cic:/Coq/Reals/Rtrigo/sin_increasing_1.con
cic:/Coq/Reals/Rtrigo/sin_lb.con
cic:/Coq/Reals/Rtrigo/sin_lb_gt_0.con
cic:/Coq/Reals/Rtrigo/sin_le_0.con
cic:/Coq/Reals/Rtrigo/sin_lt_0.con
cic:/Coq/Reals/Rtrigo/sin_minus.con
cic:/Coq/Reals/Rtrigo/sin_neg.con
cic:/Coq/Reals/Rtrigo/sin_period.con
cic:/Coq/Reals/Rtrigo/sin_plus.con
cic:/Coq/Reals/Rtrigo/sin_shift.con
cic:/Coq/Reals/Rtrigo/sin_ub.con
cic:/Coq/Reals/Rtrigo/tan.con
cic:/Coq/Reals/Rtrigo/tan_0.con
cic:/Coq/Reals/Rtrigo/tan_2a.con
cic:/Coq/Reals/Rtrigo/tan_diff.con
cic:/Coq/Reals/Rtrigo/tan_gt_0.con
cic:/Coq/Reals/Rtrigo/tan_incr_0.con
cic:/Coq/Reals/Rtrigo/tan_incr_1.con
cic:/Coq/Reals/Rtrigo/tan_increasing_0.con
cic:/Coq/Reals/Rtrigo/tan_increasing_1.con
cic:/Coq/Reals/Rtrigo/tan_lt_0.con
cic:/Coq/Reals/Rtrigo/tan_minus.con
cic:/Coq/Reals/Rtrigo/tan_neg.con
cic:/Coq/Reals/Rtrigo/tan_plus.con
cic:/Coq/Reals/Rtrigo_alt/PI_4.con
cic:/Coq/Reals/Rtrigo_alt/cos_approx.con
cic:/Coq/Reals/Rtrigo_alt/cos_bound.con
cic:/Coq/Reals/Rtrigo_alt/cos_term.con
cic:/Coq/Reals/Rtrigo_alt/sin_approx.con
cic:/Coq/Reals/Rtrigo_alt/sin_bound.con
cic:/Coq/Reals/Rtrigo_alt/sin_term.con
cic:/Coq/Reals/Rtrigo_calc/PI4_RGT_0.con
cic:/Coq/Reals/Rtrigo_calc/PI6_RGT_0.con
cic:/Coq/Reals/Rtrigo_calc/PI6_RLT_PI2.con
cic:/Coq/Reals/Rtrigo_calc/R1_sqrt2_neq_0.con
cic:/Coq/Reals/Rtrigo_calc/Rgt_2PI_0.con
cic:/Coq/Reals/Rtrigo_calc/Rgt_3PI2_0.con
cic:/Coq/Reals/Rtrigo_calc/Rlt_3PI2_2PI.con
cic:/Coq/Reals/Rtrigo_calc/Rlt_PI_3PI2.con
cic:/Coq/Reals/Rtrigo_calc/Rlt_sqrt2_0.con
cic:/Coq/Reals/Rtrigo_calc/Rlt_sqrt3_0.con
cic:/Coq/Reals/Rtrigo_calc/Rsqr_sin_cos_d_one.con
cic:/Coq/Reals/Rtrigo_calc/cos3PI4.con
cic:/Coq/Reals/Rtrigo_calc/cos_2PI3.con
cic:/Coq/Reals/Rtrigo_calc/cos_5PI4.con
cic:/Coq/Reals/Rtrigo_calc/cos_PI3.con
cic:/Coq/Reals/Rtrigo_calc/cos_PI4.con
cic:/Coq/Reals/Rtrigo_calc/cos_PI6.con
cic:/Coq/Reals/Rtrigo_calc/cosd.con
cic:/Coq/Reals/Rtrigo_calc/deg_rad.con
cic:/Coq/Reals/Rtrigo_calc/plat.con
cic:/Coq/Reals/Rtrigo_calc/rad_deg.con
cic:/Coq/Reals/Rtrigo_calc/sin3PI4.con
cic:/Coq/Reals/Rtrigo_calc/sin_2PI3.con
cic:/Coq/Reals/Rtrigo_calc/sin_3PI2.con
cic:/Coq/Reals/Rtrigo_calc/sin_5PI4.con
cic:/Coq/Reals/Rtrigo_calc/sin_PI3.con
cic:/Coq/Reals/Rtrigo_calc/sin_PI3_cos_PI6.con
cic:/Coq/Reals/Rtrigo_calc/sin_PI4.con
cic:/Coq/Reals/Rtrigo_calc/sin_PI6.con
cic:/Coq/Reals/Rtrigo_calc/sin_PI6_cos_PI3.con
cic:/Coq/Reals/Rtrigo_calc/sin_cos5PI4.con
cic:/Coq/Reals/Rtrigo_calc/sin_cos_PI4.con
cic:/Coq/Reals/Rtrigo_calc/sin_lb_ge_0.con
cic:/Coq/Reals/Rtrigo_calc/sind.con
cic:/Coq/Reals/Rtrigo_calc/sqrt2_neq_0.con
cic:/Coq/Reals/Rtrigo_calc/sqrt3_2_neq_0.con
cic:/Coq/Reals/Rtrigo_calc/tan_2PI.con
cic:/Coq/Reals/Rtrigo_calc/tan_2PI3.con
cic:/Coq/Reals/Rtrigo_calc/tan_PI.con
cic:/Coq/Reals/Rtrigo_calc/tan_PI3.con
cic:/Coq/Reals/Rtrigo_calc/tan_PI6.con
cic:/Coq/Reals/Rtrigo_calc/tand.con
cic:/Coq/Reals/Rtrigo_calc/toDeg.con
cic:/Coq/Reals/Rtrigo_calc/toRad.con
cic:/Coq/Reals/Rtrigo_calc/toRad_inj.con
cic:/Coq/Reals/Rtrigo_def/Alembert_cos.con
cic:/Coq/Reals/Rtrigo_def/Alembert_sin.con
cic:/Coq/Reals/Rtrigo_def/archimed_cor1.con
cic:/Coq/Reals/Rtrigo_def/cos.con
cic:/Coq/Reals/Rtrigo_def/cos_0.con
cic:/Coq/Reals/Rtrigo_def/cos_in.con
cic:/Coq/Reals/Rtrigo_def/cos_n.con
cic:/Coq/Reals/Rtrigo_def/cos_sym.con
cic:/Coq/Reals/Rtrigo_def/cosh.con
cic:/Coq/Reals/Rtrigo_def/cosh_0.con
cic:/Coq/Reals/Rtrigo_def/cosn_no_R0.con
cic:/Coq/Reals/Rtrigo_def/exist_cos.con
cic:/Coq/Reals/Rtrigo_def/exist_cos0.con
cic:/Coq/Reals/Rtrigo_def/exist_exp.con
cic:/Coq/Reals/Rtrigo_def/exist_exp0.con
cic:/Coq/Reals/Rtrigo_def/exist_sin.con
cic:/Coq/Reals/Rtrigo_def/exp.con
cic:/Coq/Reals/Rtrigo_def/exp_0.con
cic:/Coq/Reals/Rtrigo_def/exp_cof_no_R0.con
cic:/Coq/Reals/Rtrigo_def/exp_in.con
cic:/Coq/Reals/Rtrigo_def/pow_i.con
cic:/Coq/Reals/Rtrigo_def/simpl_cos_n.con
cic:/Coq/Reals/Rtrigo_def/simpl_sin_n.con
cic:/Coq/Reals/Rtrigo_def/sin.con
cic:/Coq/Reals/Rtrigo_def/sin_0.con
cic:/Coq/Reals/Rtrigo_def/sin_antisym.con
cic:/Coq/Reals/Rtrigo_def/sin_in.con
cic:/Coq/Reals/Rtrigo_def/sin_n.con
cic:/Coq/Reals/Rtrigo_def/sin_no_R0.con
cic:/Coq/Reals/Rtrigo_def/sinh.con
cic:/Coq/Reals/Rtrigo_def/sinh_0.con
cic:/Coq/Reals/Rtrigo_def/tanh.con
cic:/Coq/Reals/Rtrigo_fun/Alembert_exp.con
cic:/Coq/Reals/Rtrigo_reg/CVN_R_cos.con
cic:/Coq/Reals/Rtrigo_reg/CVN_R_sin.con
cic:/Coq/Reals/Rtrigo_reg/continuity_cos.con
cic:/Coq/Reals/Rtrigo_reg/continuity_sin.con
cic:/Coq/Reals/Rtrigo_reg/derivable_cos.con
cic:/Coq/Reals/Rtrigo_reg/derivable_pt_cos.con
cic:/Coq/Reals/Rtrigo_reg/derivable_pt_lim_sin.con
cic:/Coq/Reals/Rtrigo_reg/derivable_pt_lim_sin_0.con
cic:/Coq/Reals/Rtrigo_reg/derivable_pt_sin.con
cic:/Coq/Reals/Rtrigo_reg/derivable_sin.con
cic:/Coq/Reals/Rtrigo_reg/derive_pt_cos.con
cic:/Coq/Reals/Rtrigo_reg/derive_pt_sin.con
cic:/Coq/Reals/SeqProp/CV_Cauchy.con
cic:/Coq/Reals/SeqProp/CV_minus.con
cic:/Coq/Reals/SeqProp/CV_mult.con
cic:/Coq/Reals/SeqProp/CV_opp.con
cic:/Coq/Reals/SeqProp/CV_plus.con
cic:/Coq/Reals/SeqProp/UL_sequence.con
cic:/Coq/Reals/SeqProp/Un_decreasing.con
cic:/Coq/Reals/SeqProp/Vn_Un_Wn_order.con
cic:/Coq/Reals/SeqProp/Vn_growing.con
cic:/Coq/Reals/SeqProp/Wn_decreasing.con
cic:/Coq/Reals/SeqProp/approx_maj.con
cic:/Coq/Reals/SeqProp/approx_min.con
cic:/Coq/Reals/SeqProp/cauchy_maj.con
cic:/Coq/Reals/SeqProp/cauchy_min.con
cic:/Coq/Reals/SeqProp/cauchy_opp.con
cic:/Coq/Reals/SeqProp/cond_eq.con
cic:/Coq/Reals/SeqProp/cv_cvabs.con
cic:/Coq/Reals/SeqProp/cv_infty.con
cic:/Coq/Reals/SeqProp/cv_infty_cv_R0.con
cic:/Coq/Reals/SeqProp/cv_speed_pow_fact.con
cic:/Coq/Reals/SeqProp/decreasing_cv.con
cic:/Coq/Reals/SeqProp/decreasing_growing.con
cic:/Coq/Reals/SeqProp/decreasing_ineq.con
cic:/Coq/Reals/SeqProp/decreasing_prop.con
cic:/Coq/Reals/SeqProp/growing_cv.con
cic:/Coq/Reals/SeqProp/growing_ineq.con
cic:/Coq/Reals/SeqProp/has_lb.con
cic:/Coq/Reals/SeqProp/has_ub.con
cic:/Coq/Reals/SeqProp/maj_by_pos.con
cic:/Coq/Reals/SeqProp/maj_cv.con
cic:/Coq/Reals/SeqProp/maj_min.con
cic:/Coq/Reals/SeqProp/maj_ss.con
cic:/Coq/Reals/SeqProp/maj_sup.con
cic:/Coq/Reals/SeqProp/majorant.con
cic:/Coq/Reals/SeqProp/min_cv.con
cic:/Coq/Reals/SeqProp/min_inf.con
cic:/Coq/Reals/SeqProp/min_maj.con
cic:/Coq/Reals/SeqProp/min_ss.con
cic:/Coq/Reals/SeqProp/minorant.con
cic:/Coq/Reals/SeqProp/not_Rlt.con
cic:/Coq/Reals/SeqProp/opp_seq.con
cic:/Coq/Reals/SeqProp/sequence_majorant.con
cic:/Coq/Reals/SeqProp/sequence_minorant.con
cic:/Coq/Reals/SeqProp/tech10.con
cic:/Coq/Reals/SeqProp/tech13.con
cic:/Coq/Reals/SeqProp/tech9.con
cic:/Coq/Reals/SeqSeries/Cesaro.con
cic:/Coq/Reals/SeqSeries/Cesaro_1.con
cic:/Coq/Reals/SeqSeries/Rseries_CV_comp.con
cic:/Coq/Reals/SeqSeries/sum_maj1.con
cic:/Coq/Reals/Sqrt_reg/continuity_pt_sqrt.con
cic:/Coq/Reals/Sqrt_reg/derivable_pt_sqrt.con
cic:/Coq/Reals/Sqrt_reg/derive_pt_sqrt.con
cic:/Coq/Reals/Sqrt_reg/sqrt_continuity_pt.con
cic:/Coq/Reals/Sqrt_reg/sqrt_continuity_pt_R1.con
cic:/Coq/Reals/Sqrt_reg/sqrt_var_maj.con
cic:/Coq/Relations/Newman/Diagram.con
cic:/Coq/Relations/Newman/Ind_proof.con
cic:/Coq/Relations/Newman/Newman.con
cic:/Coq/Relations/Newman/Rstar_coherence.con
cic:/Coq/Relations/Newman/caseRxy.con
cic:/Coq/Relations/Newman/coherence.con
cic:/Coq/Relations/Newman/coherence_intro.con
cic:/Coq/Relations/Newman/coherence_sym.con
cic:/Coq/Relations/Newman/confluence.con
cic:/Coq/Relations/Newman/local_confluence.con
cic:/Coq/Relations/Newman/noetherian.con
cic:/Coq/Relations/Operators_Properties/clos_refl_trans_ind_left.con
cic:/Coq/Relations/Operators_Properties/clos_rst_idempotent.con
cic:/Coq/Relations/Operators_Properties/clos_rst_is_equiv.con
cic:/Coq/Relations/Operators_Properties/clos_rt_clos_rst.con
cic:/Coq/Relations/Operators_Properties/clos_rt_idempotent.con
cic:/Coq/Relations/Operators_Properties/clos_rt_is_preorder.con
cic:/Coq/Relations/Relation_Definitions/PER_ind.con
cic:/Coq/Relations/Relation_Definitions/PER_rec.con
cic:/Coq/Relations/Relation_Definitions/PER_rect.con
cic:/Coq/Relations/Relation_Definitions/antisymmetric.con
cic:/Coq/Relations/Relation_Definitions/commut.con
cic:/Coq/Relations/Relation_Definitions/equiv.con
cic:/Coq/Relations/Relation_Definitions/equiv_refl.con
cic:/Coq/Relations/Relation_Definitions/equiv_sym.con
cic:/Coq/Relations/Relation_Definitions/equiv_trans.con
cic:/Coq/Relations/Relation_Definitions/equivalence_ind.con
cic:/Coq/Relations/Relation_Definitions/equivalence_rec.con
cic:/Coq/Relations/Relation_Definitions/equivalence_rect.con
cic:/Coq/Relations/Relation_Definitions/inclusion.con
cic:/Coq/Relations/Relation_Definitions/ord_antisym.con
cic:/Coq/Relations/Relation_Definitions/ord_refl.con
cic:/Coq/Relations/Relation_Definitions/ord_trans.con
cic:/Coq/Relations/Relation_Definitions/order_ind.con
cic:/Coq/Relations/Relation_Definitions/order_rec.con
cic:/Coq/Relations/Relation_Definitions/order_rect.con
cic:/Coq/Relations/Relation_Definitions/per_sym.con
cic:/Coq/Relations/Relation_Definitions/per_trans.con
cic:/Coq/Relations/Relation_Definitions/preord_refl.con
cic:/Coq/Relations/Relation_Definitions/preord_trans.con
cic:/Coq/Relations/Relation_Definitions/preorder_ind.con
cic:/Coq/Relations/Relation_Definitions/preorder_rec.con
cic:/Coq/Relations/Relation_Definitions/preorder_rect.con
cic:/Coq/Relations/Relation_Definitions/reflexive.con
cic:/Coq/Relations/Relation_Definitions/relation.con
cic:/Coq/Relations/Relation_Definitions/same_relation.con
cic:/Coq/Relations/Relation_Definitions/symmetric.con
cic:/Coq/Relations/Relation_Definitions/transitive.con
cic:/Coq/Relations/Relation_Operators/Desc_ind.con
cic:/Coq/Relations/Relation_Operators/Ltl_ind.con
cic:/Coq/Relations/Relation_Operators/Pow.con
cic:/Coq/Relations/Relation_Operators/clos_refl_sym_trans_ind.con
cic:/Coq/Relations/Relation_Operators/clos_refl_trans_ind.con
cic:/Coq/Relations/Relation_Operators/clos_trans_ind.con
cic:/Coq/Relations/Relation_Operators/le_AsB_ind.con
cic:/Coq/Relations/Relation_Operators/lex_exp.con
cic:/Coq/Relations/Relation_Operators/lexprod_ind.con
cic:/Coq/Relations/Relation_Operators/swapprod_ind.con
cic:/Coq/Relations/Relation_Operators/symprod_ind.con
cic:/Coq/Relations/Relation_Operators/transp.con
cic:/Coq/Relations/Relation_Operators/union.con
cic:/Coq/Relations/Relations/inverse_image_of_eq.con
cic:/Coq/Relations/Relations/inverse_image_of_equivalence.con
cic:/Coq/Relations/Rstar/Rstar'.con
cic:/Coq/Relations/Rstar/Rstar'_R.con
cic:/Coq/Relations/Rstar/Rstar'_Rstar.con
cic:/Coq/Relations/Rstar/Rstar'_reflexive.con
cic:/Coq/Relations/Rstar/Rstar.con
cic:/Coq/Relations/Rstar/Rstar_R.con
cic:/Coq/Relations/Rstar/Rstar_Rstar'.con
cic:/Coq/Relations/Rstar/Rstar_reflexive.con
cic:/Coq/Relations/Rstar/Rstar_transitive.con
cic:/Coq/Relations/Rstar/commut.con
cic:/Coq/Setoids/Setoid/Prop_S.con
cic:/Coq/Setoids/Setoid/Seq_refl.con
cic:/Coq/Setoids/Setoid/Seq_sym.con
cic:/Coq/Setoids/Setoid/Seq_trans.con
cic:/Coq/Setoids/Setoid/Setoid_Theory_ind.con
cic:/Coq/Setoids/Setoid/Setoid_Theory_rec.con
cic:/Coq/Setoids/Setoid/Setoid_Theory_rect.con
cic:/Coq/Setoids/Setoid/and_ext.con
cic:/Coq/Setoids/Setoid/and_ext2.con
cic:/Coq/Setoids/Setoid/fleche.con
cic:/Coq/Setoids/Setoid/fleche_ext.con
cic:/Coq/Setoids/Setoid/fleche_ext2.con
cic:/Coq/Setoids/Setoid/not_ext.con
cic:/Coq/Setoids/Setoid/not_ext2.con
cic:/Coq/Setoids/Setoid/or_ext.con
cic:/Coq/Setoids/Setoid/or_ext2.con
cic:/Coq/Setoids/Setoid/setoid_eq_ext1.con
cic:/Coq/Setoids/Setoid/setoid_eq_ext2.con
cic:/Coq/Sets/Classical_sets/Complement_Complement.con
cic:/Coq/Sets/Classical_sets/Included_Strict_Included.con
cic:/Coq/Sets/Classical_sets/Inhabited_Setminus.con
cic:/Coq/Sets/Classical_sets/Strict_Included_inv.con
cic:/Coq/Sets/Classical_sets/Strict_super_set_contains_new_element.con
cic:/Coq/Sets/Classical_sets/Subtract_intro.con
cic:/Coq/Sets/Classical_sets/Subtract_inv.con
cic:/Coq/Sets/Classical_sets/not_SIncl_empty.con
cic:/Coq/Sets/Classical_sets/not_empty_Inhabited.con
cic:/Coq/Sets/Classical_sets/not_included_empty_Inhabited.con
cic:/Coq/Sets/Constructive_sets/Add_intro1.con
cic:/Coq/Sets/Constructive_sets/Add_intro2.con
cic:/Coq/Sets/Constructive_sets/Add_inv.con
cic:/Coq/Sets/Constructive_sets/Add_not_Empty.con
cic:/Coq/Sets/Constructive_sets/Couple_inv.con
cic:/Coq/Sets/Constructive_sets/Extension.con
cic:/Coq/Sets/Constructive_sets/Included_Empty.con
cic:/Coq/Sets/Constructive_sets/Inhabited_add.con
cic:/Coq/Sets/Constructive_sets/Inhabited_not_empty.con
cic:/Coq/Sets/Constructive_sets/Intersection_inv.con
cic:/Coq/Sets/Constructive_sets/Noone_in_empty.con
cic:/Coq/Sets/Constructive_sets/Setminus_intro.con
cic:/Coq/Sets/Constructive_sets/Singleton_intro.con
cic:/Coq/Sets/Constructive_sets/Singleton_inv.con
cic:/Coq/Sets/Constructive_sets/Strict_Included_intro.con
cic:/Coq/Sets/Constructive_sets/Strict_Included_strict.con
cic:/Coq/Sets/Constructive_sets/Union_inv.con
cic:/Coq/Sets/Constructive_sets/not_Empty_Add.con
cic:/Coq/Sets/Cpo/Bottom_ind.con
cic:/Coq/Sets/Cpo/Bottom_rec.con
cic:/Coq/Sets/Cpo/Bottom_rect.con
cic:/Coq/Sets/Cpo/Chain_cond.con
cic:/Coq/Sets/Cpo/Chain_ind.con
cic:/Coq/Sets/Cpo/Chain_rec.con
cic:/Coq/Sets/Cpo/Chain_rect.con
cic:/Coq/Sets/Cpo/Compatible.con
cic:/Coq/Sets/Cpo/Complete_ind.con
cic:/Coq/Sets/Cpo/Complete_rec.con
cic:/Coq/Sets/Cpo/Complete_rect.con
cic:/Coq/Sets/Cpo/Conditionally_complete_ind.con
cic:/Coq/Sets/Cpo/Conditionally_complete_rec.con
cic:/Coq/Sets/Cpo/Conditionally_complete_rect.con
cic:/Coq/Sets/Cpo/Cpo_cond.con
cic:/Coq/Sets/Cpo/Cpo_ind.con
cic:/Coq/Sets/Cpo/Cpo_rec.con
cic:/Coq/Sets/Cpo/Cpo_rect.con
cic:/Coq/Sets/Cpo/Directed_ind.con
cic:/Coq/Sets/Cpo/Directed_rec.con
cic:/Coq/Sets/Cpo/Directed_rect.con
cic:/Coq/Sets/Cpo/Glb_ind.con
cic:/Coq/Sets/Cpo/Glb_rec.con
cic:/Coq/Sets/Cpo/Glb_rect.con
cic:/Coq/Sets/Cpo/Lower_Bound_ind.con
cic:/Coq/Sets/Cpo/Lower_Bound_rec.con
cic:/Coq/Sets/Cpo/Lower_Bound_rect.con
cic:/Coq/Sets/Cpo/Lub_ind.con
cic:/Coq/Sets/Cpo/Lub_rec.con
cic:/Coq/Sets/Cpo/Lub_rect.con
cic:/Coq/Sets/Cpo/PO_of_chain.con
cic:/Coq/Sets/Cpo/PO_of_cpo.con
cic:/Coq/Sets/Cpo/Totally_ordered_ind.con
cic:/Coq/Sets/Cpo/Totally_ordered_rec.con
cic:/Coq/Sets/Cpo/Totally_ordered_rect.con
cic:/Coq/Sets/Cpo/Upper_Bound_ind.con
cic:/Coq/Sets/Cpo/Upper_Bound_rec.con
cic:/Coq/Sets/Cpo/Upper_Bound_rect.con
cic:/Coq/Sets/Ensembles/Add.con
cic:/Coq/Sets/Ensembles/Complement.con
cic:/Coq/Sets/Ensembles/Couple_ind.con
cic:/Coq/Sets/Ensembles/Disjoint_ind.con
cic:/Coq/Sets/Ensembles/Disjoint_rec.con
cic:/Coq/Sets/Ensembles/Disjoint_rect.con
cic:/Coq/Sets/Ensembles/Empty_set_ind.con
cic:/Coq/Sets/Ensembles/Empty_set_rec.con
cic:/Coq/Sets/Ensembles/Empty_set_rect.con
cic:/Coq/Sets/Ensembles/Ensemble.con
cic:/Coq/Sets/Ensembles/Extensionality_Ensembles.con
cic:/Coq/Sets/Ensembles/Full_set_ind.con
cic:/Coq/Sets/Ensembles/In.con
cic:/Coq/Sets/Ensembles/Included.con
cic:/Coq/Sets/Ensembles/Inhabited_ind.con
cic:/Coq/Sets/Ensembles/Intersection_ind.con
cic:/Coq/Sets/Ensembles/Same_set.con
cic:/Coq/Sets/Ensembles/Setminus.con
cic:/Coq/Sets/Ensembles/Singleton_ind.con
cic:/Coq/Sets/Ensembles/Singleton_rec.con
cic:/Coq/Sets/Ensembles/Singleton_rect.con
cic:/Coq/Sets/Ensembles/Strict_Included.con
cic:/Coq/Sets/Ensembles/Subtract.con
cic:/Coq/Sets/Ensembles/Triple_ind.con
cic:/Coq/Sets/Ensembles/Union_ind.con
cic:/Coq/Sets/Finite_sets/Finite_ind.con
cic:/Coq/Sets/Finite_sets/cardinal_elim.con
cic:/Coq/Sets/Finite_sets/cardinal_ind.con
cic:/Coq/Sets/Finite_sets/cardinal_invert.con
cic:/Coq/Sets/Finite_sets_facts/Add_preserves_Finite.con
cic:/Coq/Sets/Finite_sets_facts/Finite_downward_closed.con
cic:/Coq/Sets/Finite_sets_facts/G_aux.con
cic:/Coq/Sets/Finite_sets_facts/Generalized_induction_on_finite_sets.con
cic:/Coq/Sets/Finite_sets_facts/Intersection_preserves_finite.con
cic:/Coq/Sets/Finite_sets_facts/Singleton_is_finite.con
cic:/Coq/Sets/Finite_sets_facts/Union_preserves_Finite.con
cic:/Coq/Sets/Finite_sets_facts/card_Add_gen.con
cic:/Coq/Sets/Finite_sets_facts/card_soustr_1.con
cic:/Coq/Sets/Finite_sets_facts/cardinalO_empty.con
cic:/Coq/Sets/Finite_sets_facts/cardinal_Empty.con
cic:/Coq/Sets/Finite_sets_facts/cardinal_finite.con
cic:/Coq/Sets/Finite_sets_facts/cardinal_is_functional.con
cic:/Coq/Sets/Finite_sets_facts/cardinal_unicity.con
cic:/Coq/Sets/Finite_sets_facts/finite_cardinal.con
cic:/Coq/Sets/Finite_sets_facts/incl_card_le.con
cic:/Coq/Sets/Finite_sets_facts/incl_st_card_lt.con
cic:/Coq/Sets/Finite_sets_facts/inh_card_gt_O.con
cic:/Coq/Sets/Image/Im_add.con
cic:/Coq/Sets/Image/Im_def.con
cic:/Coq/Sets/Image/Im_ind.con
cic:/Coq/Sets/Image/Im_inv.con
cic:/Coq/Sets/Image/In_Image_elim.con
cic:/Coq/Sets/Image/Pigeonhole.con
cic:/Coq/Sets/Image/Pigeonhole_principle.con
cic:/Coq/Sets/Image/cardinal_Im_intro.con
cic:/Coq/Sets/Image/cardinal_decreases.con
cic:/Coq/Sets/Image/finite_image.con
cic:/Coq/Sets/Image/image_empty.con
cic:/Coq/Sets/Image/injective.con
cic:/Coq/Sets/Image/injective_preserves_cardinal.con
cic:/Coq/Sets/Image/not_injective_elim.con
cic:/Coq/Sets/Infinite_sets/Approximant_ind.con
cic:/Coq/Sets/Infinite_sets/Approximant_rec.con
cic:/Coq/Sets/Infinite_sets/Approximant_rect.con
cic:/Coq/Sets/Infinite_sets/Image_set_continuous'.con
cic:/Coq/Sets/Infinite_sets/Image_set_continuous.con
cic:/Coq/Sets/Infinite_sets/Pigeonhole_bis.con
cic:/Coq/Sets/Infinite_sets/Pigeonhole_ter.con
cic:/Coq/Sets/Infinite_sets/approximant_can_be_any_size.con
cic:/Coq/Sets/Infinite_sets/approximants_grow'.con
cic:/Coq/Sets/Infinite_sets/approximants_grow.con
cic:/Coq/Sets/Infinite_sets/make_new_approximant.con
cic:/Coq/Sets/Integers/Finite_subset_has_lub.con
cic:/Coq/Sets/Integers/Integers_has_no_ub.con
cic:/Coq/Sets/Integers/Integers_ind.con
cic:/Coq/Sets/Integers/Integers_infinite.con
cic:/Coq/Sets/Integers/le_Order.con
cic:/Coq/Sets/Integers/le_antisym.con
cic:/Coq/Sets/Integers/le_reflexive.con
cic:/Coq/Sets/Integers/le_total_order.con
cic:/Coq/Sets/Integers/le_trans.con
cic:/Coq/Sets/Integers/nat_po.con
cic:/Coq/Sets/Integers/triv_nat.con
cic:/Coq/Sets/Multiset/EmptyBag.con
cic:/Coq/Sets/Multiset/SingletonBag.con
cic:/Coq/Sets/Multiset/meq.con
cic:/Coq/Sets/Multiset/meq_congr.con
cic:/Coq/Sets/Multiset/meq_left.con
cic:/Coq/Sets/Multiset/meq_refl.con
cic:/Coq/Sets/Multiset/meq_right.con
cic:/Coq/Sets/Multiset/meq_sym.con
cic:/Coq/Sets/Multiset/meq_trans.con
cic:/Coq/Sets/Multiset/multiplicity.con
cic:/Coq/Sets/Multiset/multiset_ind.con
cic:/Coq/Sets/Multiset/multiset_rec.con
cic:/Coq/Sets/Multiset/multiset_rect.con
cic:/Coq/Sets/Multiset/multiset_twist1.con
cic:/Coq/Sets/Multiset/multiset_twist2.con
cic:/Coq/Sets/Multiset/munion.con
cic:/Coq/Sets/Multiset/munion_ass.con
cic:/Coq/Sets/Multiset/munion_comm.con
cic:/Coq/Sets/Multiset/munion_empty_left.con
cic:/Coq/Sets/Multiset/munion_empty_right.con
cic:/Coq/Sets/Multiset/munion_perm_left.con
cic:/Coq/Sets/Multiset/munion_rotate.con
cic:/Coq/Sets/Multiset/treesort_twist1.con
cic:/Coq/Sets/Multiset/treesort_twist2.con
cic:/Coq/Sets/Partial_Order/Carrier.con
cic:/Coq/Sets/Partial_Order/Carrier_of.con
cic:/Coq/Sets/Partial_Order/PO_cond1.con
cic:/Coq/Sets/Partial_Order/PO_cond2.con
cic:/Coq/Sets/Partial_Order/PO_ind.con
cic:/Coq/Sets/Partial_Order/PO_rec.con
cic:/Coq/Sets/Partial_Order/PO_rect.con
cic:/Coq/Sets/Partial_Order/Rel.con
cic:/Coq/Sets/Partial_Order/Rel_of.con
cic:/Coq/Sets/Partial_Order/Strict_Rel_Transitive.con
cic:/Coq/Sets/Partial_Order/Strict_Rel_Transitive_with_Rel.con
cic:/Coq/Sets/Partial_Order/Strict_Rel_Transitive_with_Rel_left.con
cic:/Coq/Sets/Partial_Order/Strict_Rel_of.con
cic:/Coq/Sets/Partial_Order/covers_ind.con
cic:/Coq/Sets/Partial_Order/covers_rec.con
cic:/Coq/Sets/Partial_Order/covers_rect.con
cic:/Coq/Sets/Permut/comm_left.con
cic:/Coq/Sets/Permut/comm_right.con
cic:/Coq/Sets/Permut/cong_congr.con
cic:/Coq/Sets/Permut/op_rotate.con
cic:/Coq/Sets/Permut/perm_left.con
cic:/Coq/Sets/Permut/perm_right.con
cic:/Coq/Sets/Permut/twist.con
cic:/Coq/Sets/Powerset/Empty_set_is_Bottom.con
cic:/Coq/Sets/Powerset/Empty_set_minimal.con
cic:/Coq/Sets/Powerset/Inclusion_is_an_order.con
cic:/Coq/Sets/Powerset/Inclusion_is_transitive.con
cic:/Coq/Sets/Powerset/Intersection_decreases_l.con
cic:/Coq/Sets/Powerset/Intersection_decreases_r.con
cic:/Coq/Sets/Powerset/Intersection_is_Glb.con
cic:/Coq/Sets/Powerset/Intersection_maximal.con
cic:/Coq/Sets/Powerset/Power_set_Inhabited.con
cic:/Coq/Sets/Powerset/Power_set_PO.con
cic:/Coq/Sets/Powerset/Power_set_ind.con
cic:/Coq/Sets/Powerset/Strict_Rel_is_Strict_Included.con
cic:/Coq/Sets/Powerset/Strict_inclusion_is_transitive.con
cic:/Coq/Sets/Powerset/Strict_inclusion_is_transitive_with_inclusion.con
cic:/Coq/Sets/Powerset/Strict_inclusion_is_transitive_with_inclusion_left.con
cic:/Coq/Sets/Powerset/Union_increases_l.con
cic:/Coq/Sets/Powerset/Union_increases_r.con
cic:/Coq/Sets/Powerset/Union_is_Lub.con
cic:/Coq/Sets/Powerset/Union_minimal.con
cic:/Coq/Sets/Powerset_Classical_facts/Add_covers.con
cic:/Coq/Sets/Powerset_Classical_facts/Included_Add.con
cic:/Coq/Sets/Powerset_Classical_facts/Simplify_add.con
cic:/Coq/Sets/Powerset_Classical_facts/Singleton_atomic.con
cic:/Coq/Sets/Powerset_Classical_facts/Sub_Add_new.con
cic:/Coq/Sets/Powerset_Classical_facts/add_soustr_1.con
cic:/Coq/Sets/Powerset_Classical_facts/add_soustr_2.con
cic:/Coq/Sets/Powerset_Classical_facts/add_soustr_xy.con
cic:/Coq/Sets/Powerset_Classical_facts/covers_Add.con
cic:/Coq/Sets/Powerset_Classical_facts/covers_is_Add.con
cic:/Coq/Sets/Powerset_Classical_facts/incl_soustr.con
cic:/Coq/Sets/Powerset_Classical_facts/incl_soustr_add_l.con
cic:/Coq/Sets/Powerset_Classical_facts/incl_soustr_add_r.con
cic:/Coq/Sets/Powerset_Classical_facts/incl_soustr_in.con
cic:/Coq/Sets/Powerset_Classical_facts/incl_st_add_soustr.con
cic:/Coq/Sets/Powerset_Classical_facts/less_than_singleton.con
cic:/Coq/Sets/Powerset_Classical_facts/setcover_inv.con
cic:/Coq/Sets/Powerset_Classical_facts/sincl_add_x.con
cic:/Coq/Sets/Powerset_facts/Add_commutative'.con
cic:/Coq/Sets/Powerset_facts/Add_commutative.con
cic:/Coq/Sets/Powerset_facts/Add_distributes.con
cic:/Coq/Sets/Powerset_facts/Couple_as_union.con
cic:/Coq/Sets/Powerset_facts/Distributivity'.con
cic:/Coq/Sets/Powerset_facts/Distributivity.con
cic:/Coq/Sets/Powerset_facts/Empty_set_zero'.con
cic:/Coq/Sets/Powerset_facts/Empty_set_zero.con
cic:/Coq/Sets/Powerset_facts/Intersection_commutative.con
cic:/Coq/Sets/Powerset_facts/Non_disjoint_union'.con
cic:/Coq/Sets/Powerset_facts/Non_disjoint_union.con
cic:/Coq/Sets/Powerset_facts/Triple_as_Couple.con
cic:/Coq/Sets/Powerset_facts/Triple_as_Couple_Singleton.con
cic:/Coq/Sets/Powerset_facts/Triple_as_union.con
cic:/Coq/Sets/Powerset_facts/Union_absorbs.con
cic:/Coq/Sets/Powerset_facts/Union_add.con
cic:/Coq/Sets/Powerset_facts/Union_associative.con
cic:/Coq/Sets/Powerset_facts/Union_commutative.con
cic:/Coq/Sets/Powerset_facts/Union_idempotent.con
cic:/Coq/Sets/Powerset_facts/incl_add.con
cic:/Coq/Sets/Powerset_facts/incl_add_x.con
cic:/Coq/Sets/Powerset_facts/less_than_empty.con
cic:/Coq/Sets/Powerset_facts/setcover_intro.con
cic:/Coq/Sets/Powerset_facts/singlx.con
cic:/Coq/Sets/Relations_1/Antisymmetric.con
cic:/Coq/Sets/Relations_1/Equivalence_ind.con
cic:/Coq/Sets/Relations_1/Equivalence_rec.con
cic:/Coq/Sets/Relations_1/Equivalence_rect.con
cic:/Coq/Sets/Relations_1/Order_ind.con
cic:/Coq/Sets/Relations_1/Order_rec.con
cic:/Coq/Sets/Relations_1/Order_rect.con
cic:/Coq/Sets/Relations_1/PER_ind.con
cic:/Coq/Sets/Relations_1/PER_rec.con
cic:/Coq/Sets/Relations_1/PER_rect.con
cic:/Coq/Sets/Relations_1/Preorder_ind.con
cic:/Coq/Sets/Relations_1/Preorder_rec.con
cic:/Coq/Sets/Relations_1/Preorder_rect.con
cic:/Coq/Sets/Relations_1/Reflexive.con
cic:/Coq/Sets/Relations_1/Relation.con
cic:/Coq/Sets/Relations_1/Symmetric.con
cic:/Coq/Sets/Relations_1/Transitive.con
cic:/Coq/Sets/Relations_1/contains.con
cic:/Coq/Sets/Relations_1/same_relation.con
cic:/Coq/Sets/Relations_1_facts/Complement.con
cic:/Coq/Sets/Relations_1_facts/Equiv_from_order.con
cic:/Coq/Sets/Relations_1_facts/Equiv_from_preorder.con
cic:/Coq/Sets/Relations_1_facts/Rsym_imp_notRsym.con
cic:/Coq/Sets/Relations_1_facts/cong_antisymmetric_same_relation.con
cic:/Coq/Sets/Relations_1_facts/cong_reflexive_same_relation.con
cic:/Coq/Sets/Relations_1_facts/cong_symmetric_same_relation.con
cic:/Coq/Sets/Relations_1_facts/cong_transitive_same_relation.con
cic:/Coq/Sets/Relations_1_facts/contains_is_preorder.con
cic:/Coq/Sets/Relations_1_facts/same_relation_is_equivalence.con
cic:/Coq/Sets/Relations_2/Rplus_ind.con
cic:/Coq/Sets/Relations_2/Rstar1_ind.con
cic:/Coq/Sets/Relations_2/Rstar_ind.con
cic:/Coq/Sets/Relations_2/Strongly_confluent.con
cic:/Coq/Sets/Relations_2_facts/Lemma1.con
cic:/Coq/Sets/Relations_2_facts/Rplus_contains_R.con
cic:/Coq/Sets/Relations_2_facts/RstarRplus_RRstar.con
cic:/Coq/Sets/Relations_2_facts/Rstar_cases.con
cic:/Coq/Sets/Relations_2_facts/Rstar_contains_R.con
cic:/Coq/Sets/Relations_2_facts/Rstar_contains_Rplus.con
cic:/Coq/Sets/Relations_2_facts/Rstar_equiv_Rstar1.con
cic:/Coq/Sets/Relations_2_facts/Rstar_reflexive.con
cic:/Coq/Sets/Relations_2_facts/Rstar_transitive.con
cic:/Coq/Sets/Relations_2_facts/Rsym_imp_Rstarsym.con
cic:/Coq/Sets/Relations_2_facts/Sstar_contains_Rstar.con
cic:/Coq/Sets/Relations_2_facts/star_monotone.con
cic:/Coq/Sets/Relations_3/Confluent.con
cic:/Coq/Sets/Relations_3/Locally_confluent.con
cic:/Coq/Sets/Relations_3/Noetherian.con
cic:/Coq/Sets/Relations_3/coherent.con
cic:/Coq/Sets/Relations_3/confluent.con
cic:/Coq/Sets/Relations_3/locally_confluent.con
cic:/Coq/Sets/Relations_3/noetherian_ind.con
cic:/Coq/Sets/Relations_3_facts/Newman.con
cic:/Coq/Sets/Relations_3_facts/Noetherian_contains_Noetherian.con
cic:/Coq/Sets/Relations_3_facts/Rstar_imp_coherent.con
cic:/Coq/Sets/Relations_3_facts/Strong_confluence.con
cic:/Coq/Sets/Relations_3_facts/Strong_confluence_direct.con
cic:/Coq/Sets/Relations_3_facts/coherent_symmetric.con
cic:/Coq/Sets/Uniset/Emptyset.con
cic:/Coq/Sets/Uniset/Fullset.con
cic:/Coq/Sets/Uniset/In.con
cic:/Coq/Sets/Uniset/Singleton.con
cic:/Coq/Sets/Uniset/charac.con
cic:/Coq/Sets/Uniset/incl.con
cic:/Coq/Sets/Uniset/incl_left.con
cic:/Coq/Sets/Uniset/incl_right.con
cic:/Coq/Sets/Uniset/leb_refl.con
cic:/Coq/Sets/Uniset/seq.con
cic:/Coq/Sets/Uniset/seq_congr.con
cic:/Coq/Sets/Uniset/seq_left.con
cic:/Coq/Sets/Uniset/seq_refl.con
cic:/Coq/Sets/Uniset/seq_right.con
cic:/Coq/Sets/Uniset/seq_sym.con
cic:/Coq/Sets/Uniset/seq_trans.con
cic:/Coq/Sets/Uniset/treesort_twist1.con
cic:/Coq/Sets/Uniset/treesort_twist2.con
cic:/Coq/Sets/Uniset/union.con
cic:/Coq/Sets/Uniset/union_ass.con
cic:/Coq/Sets/Uniset/union_comm.con
cic:/Coq/Sets/Uniset/union_empty_left.con
cic:/Coq/Sets/Uniset/union_empty_right.con
cic:/Coq/Sets/Uniset/union_perm_left.con
cic:/Coq/Sets/Uniset/union_rotate.con
cic:/Coq/Sets/Uniset/uniset_ind.con
cic:/Coq/Sets/Uniset/uniset_rec.con
cic:/Coq/Sets/Uniset/uniset_rect.con
cic:/Coq/Sets/Uniset/uniset_twist1.con
cic:/Coq/Sets/Uniset/uniset_twist2.con
cic:/Coq/Sorting/Heap/Tree_ind.con
cic:/Coq/Sorting/Heap/Tree_rec.con
cic:/Coq/Sorting/Heap/Tree_rect.con
cic:/Coq/Sorting/Heap/build_heap_ind.con
cic:/Coq/Sorting/Heap/build_heap_rec.con
cic:/Coq/Sorting/Heap/build_heap_rect.con
cic:/Coq/Sorting/Heap/contents.con
cic:/Coq/Sorting/Heap/equiv_Tree.con
cic:/Coq/Sorting/Heap/flat_spec_ind.con
cic:/Coq/Sorting/Heap/flat_spec_rec.con
cic:/Coq/Sorting/Heap/flat_spec_rect.con
cic:/Coq/Sorting/Heap/heap_to_list.con
cic:/Coq/Sorting/Heap/insert.con
cic:/Coq/Sorting/Heap/insert_spec_ind.con
cic:/Coq/Sorting/Heap/insert_spec_rec.con
cic:/Coq/Sorting/Heap/insert_spec_rect.con
cic:/Coq/Sorting/Heap/invert_heap.con
cic:/Coq/Sorting/Heap/is_heap_ind.con
cic:/Coq/Sorting/Heap/is_heap_rec.con
cic:/Coq/Sorting/Heap/leA_Tree.con
cic:/Coq/Sorting/Heap/leA_Tree_Leaf.con
cic:/Coq/Sorting/Heap/leA_Tree_Node.con
cic:/Coq/Sorting/Heap/list_to_heap.con
cic:/Coq/Sorting/Heap/low_trans.con
cic:/Coq/Sorting/Heap/treesort.con
cic:/Coq/Sorting/Permutation/list_contents.con
cic:/Coq/Sorting/Permutation/list_contents_app.con
cic:/Coq/Sorting/Permutation/permut_app.con
cic:/Coq/Sorting/Permutation/permut_cons.con
cic:/Coq/Sorting/Permutation/permut_middle.con
cic:/Coq/Sorting/Permutation/permut_refl.con
cic:/Coq/Sorting/Permutation/permut_right.con
cic:/Coq/Sorting/Permutation/permut_tran.con
cic:/Coq/Sorting/Permutation/permutation.con
cic:/Coq/Sorting/Sorting/lelistA_ind.con
cic:/Coq/Sorting/Sorting/lelistA_inv.con
cic:/Coq/Sorting/Sorting/merge.con
cic:/Coq/Sorting/Sorting/merge_lem_ind.con
cic:/Coq/Sorting/Sorting/merge_lem_rec.con
cic:/Coq/Sorting/Sorting/merge_lem_rect.con
cic:/Coq/Sorting/Sorting/sort_ind.con
cic:/Coq/Sorting/Sorting/sort_inv.con
cic:/Coq/Sorting/Sorting/sort_rec.con
cic:/Coq/Wellfounded/Disjoint_Union/acc_A_sum.con
cic:/Coq/Wellfounded/Disjoint_Union/acc_B_sum.con
cic:/Coq/Wellfounded/Disjoint_Union/wf_disjoint_sum.con
cic:/Coq/Wellfounded/Inclusion/Acc_incl.con
cic:/Coq/Wellfounded/Inclusion/wf_incl.con
cic:/Coq/Wellfounded/Inverse_Image/Acc_inverse_image.con
cic:/Coq/Wellfounded/Inverse_Image/Acc_inverse_rel.con
cic:/Coq/Wellfounded/Inverse_Image/Acc_lemma.con
cic:/Coq/Wellfounded/Inverse_Image/wf_inverse_image.con
cic:/Coq/Wellfounded/Inverse_Image/wf_inverse_rel.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/acc_app.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/desc_end.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/desc_prefix.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/desc_tail.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/dist_Desc_concat.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/dist_aux.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/left_prefix.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/ltl_unit.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/right_prefix.con
cic:/Coq/Wellfounded/Lexicographic_Exponentiation/wf_lex_exp.con
cic:/Coq/Wellfounded/Lexicographic_Product/Acc_swapprod.con
cic:/Coq/Wellfounded/Lexicographic_Product/Acc_symprod.con
cic:/Coq/Wellfounded/Lexicographic_Product/acc_A_B_lexprod.con
cic:/Coq/Wellfounded/Lexicographic_Product/swap_Acc.con
cic:/Coq/Wellfounded/Lexicographic_Product/wf_lexprod.con
cic:/Coq/Wellfounded/Lexicographic_Product/wf_swapprod.con
cic:/Coq/Wellfounded/Lexicographic_Product/wf_symprod.con
cic:/Coq/Wellfounded/Transitive_Closure/Acc_clos_trans.con
cic:/Coq/Wellfounded/Transitive_Closure/Acc_inv_trans.con
cic:/Coq/Wellfounded/Transitive_Closure/incl_clos_trans.con
cic:/Coq/Wellfounded/Transitive_Closure/wf_clos_trans.con
cic:/Coq/Wellfounded/Union/Acc_union.con
cic:/Coq/Wellfounded/Union/strip_commut.con
cic:/Coq/Wellfounded/Union/wf_union.con
cic:/Coq/Wellfounded/Well_Ordering/B.con
cic:/Coq/Wellfounded/Well_Ordering/WO_ind.con
cic:/Coq/Wellfounded/Well_Ordering/WO_rec.con
cic:/Coq/Wellfounded/Well_Ordering/WO_rect.con
cic:/Coq/Wellfounded/Well_Ordering/le_WO_ind.con
cic:/Coq/Wellfounded/Well_Ordering/wf_WO.con
cic:/Coq/Wellfounded/Well_Ordering/wof.con
cic:/Coq/ZArith/BinInt/ZL0.con
cic:/Coq/ZArith/BinInt/ZPminus.con
cic:/Coq/ZArith/BinInt/Z_eq_mult.con
cic:/Coq/ZArith/BinInt/Z_ind.con
cic:/Coq/ZArith/BinInt/Z_of_N.con
cic:/Coq/ZArith/BinInt/Z_of_nat.con
cic:/Coq/ZArith/BinInt/Z_rec.con
cic:/Coq/ZArith/BinInt/Z_rect.con
cic:/Coq/ZArith/BinInt/Zabs.con
cic:/Coq/ZArith/BinInt/Zabs_N.con
cic:/Coq/ZArith/BinInt/Zabs_nat.con
cic:/Coq/ZArith/BinInt/Zcompare.con
cic:/Coq/ZArith/BinInt/Zdouble.con
cic:/Coq/ZArith/BinInt/Zdouble_minus_one.con
cic:/Coq/ZArith/BinInt/Zdouble_plus_one.con
cic:/Coq/ZArith/BinInt/Zeq_minus.con
cic:/Coq/ZArith/BinInt/Zge.con
cic:/Coq/ZArith/BinInt/Zgt.con
cic:/Coq/ZArith/BinInt/Zind.con
cic:/Coq/ZArith/BinInt/Zle.con
cic:/Coq/ZArith/BinInt/Zlt.con
cic:/Coq/ZArith/BinInt/Zminus.con
cic:/Coq/ZArith/BinInt/Zminus_0_l_reverse.con
cic:/Coq/ZArith/BinInt/Zminus_0_r.con
cic:/Coq/ZArith/BinInt/Zminus_diag.con
cic:/Coq/ZArith/BinInt/Zminus_diag_reverse.con
cic:/Coq/ZArith/BinInt/Zminus_eq.con
cic:/Coq/ZArith/BinInt/Zminus_plus.con
cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_l.con
cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_l_reverse.con
cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_r.con
cic:/Coq/ZArith/BinInt/Zminus_succ_l.con
cic:/Coq/ZArith/BinInt/Zmult.con
cic:/Coq/ZArith/BinInt/Zmult_0_l.con
cic:/Coq/ZArith/BinInt/Zmult_0_r.con
cic:/Coq/ZArith/BinInt/Zmult_0_r_reverse.con
cic:/Coq/ZArith/BinInt/Zmult_1_inversion_l.con
cic:/Coq/ZArith/BinInt/Zmult_1_l.con
cic:/Coq/ZArith/BinInt/Zmult_1_r.con
cic:/Coq/ZArith/BinInt/Zmult_assoc.con
cic:/Coq/ZArith/BinInt/Zmult_assoc_reverse.con
cic:/Coq/ZArith/BinInt/Zmult_comm.con
cic:/Coq/ZArith/BinInt/Zmult_integral.con
cic:/Coq/ZArith/BinInt/Zmult_integral_l.con
cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con
cic:/Coq/ZArith/BinInt/Zmult_minus_distr_r.con
cic:/Coq/ZArith/BinInt/Zmult_opp_comm.con
cic:/Coq/ZArith/BinInt/Zmult_opp_opp.con
cic:/Coq/ZArith/BinInt/Zmult_permute.con
cic:/Coq/ZArith/BinInt/Zmult_plus_distr_l.con
cic:/Coq/ZArith/BinInt/Zmult_plus_distr_r.con
cic:/Coq/ZArith/BinInt/Zmult_reg_l.con
cic:/Coq/ZArith/BinInt/Zmult_reg_r.con
cic:/Coq/ZArith/BinInt/Zmult_succ_l.con
cic:/Coq/ZArith/BinInt/Zmult_succ_l_reverse.con
cic:/Coq/ZArith/BinInt/Zmult_succ_r.con
cic:/Coq/ZArith/BinInt/Zmult_succ_r_reverse.con
cic:/Coq/ZArith/BinInt/Zne.con
cic:/Coq/ZArith/BinInt/Zneg_plus_distr.con
cic:/Coq/ZArith/BinInt/Zneg_xI.con
cic:/Coq/ZArith/BinInt/Zneg_xO.con
cic:/Coq/ZArith/BinInt/Zopp.con
cic:/Coq/ZArith/BinInt/Zopp_eq_mult_neg_1.con
cic:/Coq/ZArith/BinInt/Zopp_inj.con
cic:/Coq/ZArith/BinInt/Zopp_involutive.con
cic:/Coq/ZArith/BinInt/Zopp_mult_distr_l.con
cic:/Coq/ZArith/BinInt/Zopp_mult_distr_l_reverse.con
cic:/Coq/ZArith/BinInt/Zopp_mult_distr_r.con
cic:/Coq/ZArith/BinInt/Zopp_neg.con
cic:/Coq/ZArith/BinInt/Zopp_plus_distr.con
cic:/Coq/ZArith/BinInt/Zplus'.con
cic:/Coq/ZArith/BinInt/Zplus.con
cic:/Coq/ZArith/BinInt/Zplus_0_l.con
cic:/Coq/ZArith/BinInt/Zplus_0_r.con
cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con
cic:/Coq/ZArith/BinInt/Zplus_0_simpl_l.con
cic:/Coq/ZArith/BinInt/Zplus_0_simpl_l_reverse.con
cic:/Coq/ZArith/BinInt/Zplus_assoc.con
cic:/Coq/ZArith/BinInt/Zplus_assoc_reverse.con
cic:/Coq/ZArith/BinInt/Zplus_comm.con
cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con
cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con
cic:/Coq/ZArith/BinInt/Zplus_minus.con
cic:/Coq/ZArith/BinInt/Zplus_minus_eq.con
cic:/Coq/ZArith/BinInt/Zplus_opp_expand.con
cic:/Coq/ZArith/BinInt/Zplus_opp_l.con
cic:/Coq/ZArith/BinInt/Zplus_opp_r.con
cic:/Coq/ZArith/BinInt/Zplus_permute.con
cic:/Coq/ZArith/BinInt/Zplus_reg_l.con
cic:/Coq/ZArith/BinInt/Zplus_succ_comm.con
cic:/Coq/ZArith/BinInt/Zplus_succ_l.con
cic:/Coq/ZArith/BinInt/Zplus_succ_r.con
cic:/Coq/ZArith/BinInt/Zpos_plus_distr.con
cic:/Coq/ZArith/BinInt/Zpos_succ_morphism.con
cic:/Coq/ZArith/BinInt/Zpos_xI.con
cic:/Coq/ZArith/BinInt/Zpos_xO.con
cic:/Coq/ZArith/BinInt/Zpred'.con
cic:/Coq/ZArith/BinInt/Zpred'_succ'.con
cic:/Coq/ZArith/BinInt/Zpred.con
cic:/Coq/ZArith/BinInt/Zpred_succ.con
cic:/Coq/ZArith/BinInt/Zsgn.con
cic:/Coq/ZArith/BinInt/Zsucc'.con
cic:/Coq/ZArith/BinInt/Zsucc'_discr.con
cic:/Coq/ZArith/BinInt/Zsucc.con
cic:/Coq/ZArith/BinInt/Zsucc_discr.con
cic:/Coq/ZArith/BinInt/Zsucc_eq_compat.con
cic:/Coq/ZArith/BinInt/Zsucc_inj.con
cic:/Coq/ZArith/BinInt/Zsucc_inj_contrapositive.con
cic:/Coq/ZArith/BinInt/Zsucc_pred.con
cic:/Coq/ZArith/BinInt/weak_Zmult_plus_distr_r.con
cic:/Coq/ZArith/BinInt/weak_assoc.con
cic:/Coq/ZArith/Wf_Z/ZL4_inf.con
cic:/Coq/ZArith/Wf_Z/Z_lt_induction.con
cic:/Coq/ZArith/Wf_Z/Z_lt_rec.con
cic:/Coq/ZArith/Wf_Z/Z_of_nat_complete.con
cic:/Coq/ZArith/Wf_Z/Z_of_nat_complete_inf.con
cic:/Coq/ZArith/Wf_Z/Z_of_nat_prop.con
cic:/Coq/ZArith/Wf_Z/Z_of_nat_set.con
cic:/Coq/ZArith/Wf_Z/natlike_ind.con
cic:/Coq/ZArith/Wf_Z/natlike_rec.con
cic:/Coq/ZArith/Wf_Z/natlike_rec2.con
cic:/Coq/ZArith/Wf_Z/natlike_rec3.con
cic:/Coq/ZArith/ZArith_dec/Dcompare_inf.con
cic:/Coq/ZArith/ZArith_dec/Z_dec'.con
cic:/Coq/ZArith/ZArith_dec/Z_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_eq_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_ge_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_ge_lt_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_gt_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_gt_le_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_le_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_le_gt_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_le_lt_eq_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_lt_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_lt_ge_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_lt_le_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_noteq_dec.con
cic:/Coq/ZArith/ZArith_dec/Z_notzerop.con
cic:/Coq/ZArith/ZArith_dec/Z_zerop.con
cic:/Coq/ZArith/ZArith_dec/Zcompare_rec.con
cic:/Coq/ZArith/ZArith_dec/Zlt_cotrans.con
cic:/Coq/ZArith/ZArith_dec/Zlt_cotrans_neg.con
cic:/Coq/ZArith/ZArith_dec/Zlt_cotrans_pos.con
cic:/Coq/ZArith/ZArith_dec/not_Zeq_inf.con
cic:/Coq/ZArith/Zabs/Zabs_Zmult.con
cic:/Coq/ZArith/Zabs/Zabs_Zopp.con
cic:/Coq/ZArith/Zabs/Zabs_Zsgn.con
cic:/Coq/ZArith/Zabs/Zabs_dec.con
cic:/Coq/ZArith/Zabs/Zabs_eq.con
cic:/Coq/ZArith/Zabs/Zabs_eq_case.con
cic:/Coq/ZArith/Zabs/Zabs_ind.con
cic:/Coq/ZArith/Zabs/Zabs_intro.con
cic:/Coq/ZArith/Zabs/Zabs_nat_lt.con
cic:/Coq/ZArith/Zabs/Zabs_non_eq.con
cic:/Coq/ZArith/Zabs/Zabs_pos.con
cic:/Coq/ZArith/Zabs/Zabs_triangle.con
cic:/Coq/ZArith/Zabs/Zsgn_Zabs.con
cic:/Coq/ZArith/Zbinary/Pdiv2.con
cic:/Coq/ZArith/Zbinary/Z_div2_value.con
cic:/Coq/ZArith/Zbinary/Z_to_binary.con
cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn.con
cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn_z.con
cic:/Coq/ZArith/Zbinary/Z_to_binary_to_Z.con
cic:/Coq/ZArith/Zbinary/Z_to_two_compl.con
cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn.con
cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn_z.con
cic:/Coq/ZArith/Zbinary/Z_to_two_compl_to_Z.con
cic:/Coq/ZArith/Zbinary/Zdiv2_two_power_nat.con
cic:/Coq/ZArith/Zbinary/Zeven_bit_value.con
cic:/Coq/ZArith/Zbinary/Zge_minus_two_power_nat_S.con
cic:/Coq/ZArith/Zbinary/Zlt_two_power_nat_S.con
cic:/Coq/ZArith/Zbinary/Zmod2.con
cic:/Coq/ZArith/Zbinary/Zmod2_twice.con
cic:/Coq/ZArith/Zbinary/Zodd_bit_value.con
cic:/Coq/ZArith/Zbinary/binary_to_Z_to_binary.con
cic:/Coq/ZArith/Zbinary/binary_value.con
cic:/Coq/ZArith/Zbinary/binary_value_Sn.con
cic:/Coq/ZArith/Zbinary/binary_value_pos.con
cic:/Coq/ZArith/Zbinary/binary_value_pos_subproof.con
cic:/Coq/ZArith/Zbinary/bit_value.con
cic:/Coq/ZArith/Zbinary/two_compl_to_Z_to_two_compl.con
cic:/Coq/ZArith/Zbinary/two_compl_value.con
cic:/Coq/ZArith/Zbinary/two_compl_value_Sn.con
cic:/Coq/ZArith/Zbool/Z_eq_bool.con
cic:/Coq/ZArith/Zbool/Z_ge_lt_bool.con
cic:/Coq/ZArith/Zbool/Z_gt_le_bool.con
cic:/Coq/ZArith/Zbool/Z_le_gt_bool.con
cic:/Coq/ZArith/Zbool/Z_lt_ge_bool.con
cic:/Coq/ZArith/Zbool/Z_noteq_bool.con
cic:/Coq/ZArith/Zbool/Zeq_bool.con
cic:/Coq/ZArith/Zbool/Zeven_odd_bool.con
cic:/Coq/ZArith/Zbool/Zge_bool.con
cic:/Coq/ZArith/Zbool/Zge_cases.con
cic:/Coq/ZArith/Zbool/Zge_is_le_bool.con
cic:/Coq/ZArith/Zbool/Zgt_bool.con
cic:/Coq/ZArith/Zbool/Zgt_cases.con
cic:/Coq/ZArith/Zbool/Zgt_is_le_bool.con
cic:/Coq/ZArith/Zbool/Zle_bool.con
cic:/Coq/ZArith/Zbool/Zle_bool_antisym.con
cic:/Coq/ZArith/Zbool/Zle_bool_imp_le.con
cic:/Coq/ZArith/Zbool/Zle_bool_plus_mono.con
cic:/Coq/ZArith/Zbool/Zle_bool_refl.con
cic:/Coq/ZArith/Zbool/Zle_bool_total.con
cic:/Coq/ZArith/Zbool/Zle_bool_trans.con
cic:/Coq/ZArith/Zbool/Zle_cases.con
cic:/Coq/ZArith/Zbool/Zle_imp_le_bool.con
cic:/Coq/ZArith/Zbool/Zle_is_le_bool.con
cic:/Coq/ZArith/Zbool/Zlt_bool.con
cic:/Coq/ZArith/Zbool/Zlt_cases.con
cic:/Coq/ZArith/Zbool/Zlt_is_le_bool.con
cic:/Coq/ZArith/Zbool/Zneq_bool.con
cic:/Coq/ZArith/Zbool/Zone_min_pos.con
cic:/Coq/ZArith/Zbool/Zone_pos.con
cic:/Coq/ZArith/Zcompare/Zcompare_Eq_eq.con
cic:/Coq/ZArith/Zcompare/Zcompare_Eq_iff_eq.con
cic:/Coq/ZArith/Zcompare/Zcompare_Gt_Lt_antisym.con
cic:/Coq/ZArith/Zcompare/Zcompare_Gt_not_Lt.con
cic:/Coq/ZArith/Zcompare/Zcompare_Gt_spec.con
cic:/Coq/ZArith/Zcompare/Zcompare_Gt_trans.con
cic:/Coq/ZArith/Zcompare/Zcompare_antisym.con
cic:/Coq/ZArith/Zcompare/Zcompare_egal_dec.con
cic:/Coq/ZArith/Zcompare/Zcompare_elim.con
cic:/Coq/ZArith/Zcompare/Zcompare_eq_case.con
cic:/Coq/ZArith/Zcompare/Zcompare_mult_compat.con
cic:/Coq/ZArith/Zcompare/Zcompare_opp.con
cic:/Coq/ZArith/Zcompare/Zcompare_plus_compat.con
cic:/Coq/ZArith/Zcompare/Zcompare_refl.con
cic:/Coq/ZArith/Zcompare/Zcompare_succ_Gt.con
cic:/Coq/ZArith/Zcompare/Zcompare_succ_compat.con
cic:/Coq/ZArith/Zcompare/Zge_compare.con
cic:/Coq/ZArith/Zcompare/Zgt_compare.con
cic:/Coq/ZArith/Zcompare/Zle_compare.con
cic:/Coq/ZArith/Zcompare/Zlt_compare.con
cic:/Coq/ZArith/Zcompare/Zmult_compare_compat_l.con
cic:/Coq/ZArith/Zcompare/Zmult_compare_compat_r.con
cic:/Coq/ZArith/Zcompare/Zplus_compare_compat.con
cic:/Coq/ZArith/Zcompare/rename.con
cic:/Coq/ZArith/Zcompare/weak_Zcompare_Zplus_compatible.con
cic:/Coq/ZArith/Zcompare/weaken_Zcompare_Zplus_compatible.con
cic:/Coq/ZArith/Zcomplements/Z_lt_abs_induction.con
cic:/Coq/ZArith/Zcomplements/Z_lt_abs_induction_subproof.con
cic:/Coq/ZArith/Zcomplements/Z_lt_abs_rec.con
cic:/Coq/ZArith/Zcomplements/Z_lt_abs_rec_subproof.con
cic:/Coq/ZArith/Zcomplements/Zcase_sign.con
cic:/Coq/ZArith/Zcomplements/Zlength.con
cic:/Coq/ZArith/Zcomplements/Zlength_aux.con
cic:/Coq/ZArith/Zcomplements/Zlength_cons.con
cic:/Coq/ZArith/Zcomplements/Zlength_correct.con
cic:/Coq/ZArith/Zcomplements/Zlength_correct_subproof.con
cic:/Coq/ZArith/Zcomplements/Zlength_nil.con
cic:/Coq/ZArith/Zcomplements/Zlength_nil_inv.con
cic:/Coq/ZArith/Zcomplements/floor.con
cic:/Coq/ZArith/Zcomplements/floor_gt0.con
cic:/Coq/ZArith/Zcomplements/floor_ok.con
cic:/Coq/ZArith/Zcomplements/floor_pos.con
cic:/Coq/ZArith/Zcomplements/sqr_pos.con
cic:/Coq/ZArith/Zcomplements/two_or_two_plus_one.con
cic:/Coq/ZArith/Zdiv/Z_div_POS_ge0.con
cic:/Coq/ZArith/Zdiv/Z_div_exact_1.con
cic:/Coq/ZArith/Zdiv/Z_div_exact_2.con
cic:/Coq/ZArith/Zdiv/Z_div_ge.con
cic:/Coq/ZArith/Zdiv/Z_div_ge0.con
cic:/Coq/ZArith/Zdiv/Z_div_ge0_subproof.con
cic:/Coq/ZArith/Zdiv/Z_div_lt.con
cic:/Coq/ZArith/Zdiv/Z_div_mod.con
cic:/Coq/ZArith/Zdiv/Z_div_mod_POS.con
cic:/Coq/ZArith/Zdiv/Z_div_mod_eq.con
cic:/Coq/ZArith/Zdiv/Z_div_mult.con
cic:/Coq/ZArith/Zdiv/Z_div_plus.con
cic:/Coq/ZArith/Zdiv/Z_div_same.con
cic:/Coq/ZArith/Zdiv/Z_mod_lt.con
cic:/Coq/ZArith/Zdiv/Z_mod_plus.con
cic:/Coq/ZArith/Zdiv/Z_mod_same.con
cic:/Coq/ZArith/Zdiv/Z_mod_zero_opp.con
cic:/Coq/ZArith/Zdiv/Z_mult_div_ge.con
cic:/Coq/ZArith/Zdiv/Zdiv.con
cic:/Coq/ZArith/Zdiv/Zdiv_eucl.con
cic:/Coq/ZArith/Zdiv/Zdiv_eucl_POS.con
cic:/Coq/ZArith/Zdiv/Zdiv_eucl_exist.con
cic:/Coq/ZArith/Zdiv/Zdiv_eucl_extended.con
cic:/Coq/ZArith/Zdiv/Zmod.con
cic:/Coq/ZArith/Zeven/Z_modulo_2.con
cic:/Coq/ZArith/Zeven/Zdiv2.con
cic:/Coq/ZArith/Zeven/Zeven.con
cic:/Coq/ZArith/Zeven/Zeven_Sn.con
cic:/Coq/ZArith/Zeven/Zeven_bool.con
cic:/Coq/ZArith/Zeven/Zeven_dec.con
cic:/Coq/ZArith/Zeven/Zeven_div2.con
cic:/Coq/ZArith/Zeven/Zeven_not_Zodd.con
cic:/Coq/ZArith/Zeven/Zeven_odd_dec.con
cic:/Coq/ZArith/Zeven/Zeven_pred.con
cic:/Coq/ZArith/Zeven/Zodd.con
cic:/Coq/ZArith/Zeven/Zodd_Sn.con
cic:/Coq/ZArith/Zeven/Zodd_bool.con
cic:/Coq/ZArith/Zeven/Zodd_dec.con
cic:/Coq/ZArith/Zeven/Zodd_div2.con
cic:/Coq/ZArith/Zeven/Zodd_div2_neg.con
cic:/Coq/ZArith/Zeven/Zodd_not_Zeven.con
cic:/Coq/ZArith/Zeven/Zodd_pred.con
cic:/Coq/ZArith/Zeven/Zsplit2.con
cic:/Coq/ZArith/Zlogarithm/Is_power.con
cic:/Coq/ZArith/Zlogarithm/Is_power_correct.con
cic:/Coq/ZArith/Zlogarithm/Is_power_or.con
cic:/Coq/ZArith/Zlogarithm/N_digits.con
cic:/Coq/ZArith/Zlogarithm/ZERO_le_N_digits.con
cic:/Coq/ZArith/Zlogarithm/log_inf.con
cic:/Coq/ZArith/Zlogarithm/log_inf_correct.con
cic:/Coq/ZArith/Zlogarithm/log_inf_correct1.con
cic:/Coq/ZArith/Zlogarithm/log_inf_correct2.con
cic:/Coq/ZArith/Zlogarithm/log_inf_le_log_sup.con
cic:/Coq/ZArith/Zlogarithm/log_inf_shift_nat.con
cic:/Coq/ZArith/Zlogarithm/log_near.con
cic:/Coq/ZArith/Zlogarithm/log_near_correct1.con
cic:/Coq/ZArith/Zlogarithm/log_near_correct2.con
cic:/Coq/ZArith/Zlogarithm/log_near_correct2_subproof.con
cic:/Coq/ZArith/Zlogarithm/log_sup.con
cic:/Coq/ZArith/Zlogarithm/log_sup_correct1.con
cic:/Coq/ZArith/Zlogarithm/log_sup_correct2.con
cic:/Coq/ZArith/Zlogarithm/log_sup_le_Slog_inf.con
cic:/Coq/ZArith/Zlogarithm/log_sup_log_inf.con
cic:/Coq/ZArith/Zlogarithm/log_sup_shift_nat.con
cic:/Coq/ZArith/Zmin/Zle_min_l.con
cic:/Coq/ZArith/Zmin/Zle_min_r.con
cic:/Coq/ZArith/Zmin/Zmax.con
cic:/Coq/ZArith/Zmin/Zmax1.con
cic:/Coq/ZArith/Zmin/Zmax2.con
cic:/Coq/ZArith/Zmin/Zmin.con
cic:/Coq/ZArith/Zmin/Zmin_SS.con
cic:/Coq/ZArith/Zmin/Zmin_case.con
cic:/Coq/ZArith/Zmin/Zmin_n_n.con
cic:/Coq/ZArith/Zmin/Zmin_or.con
cic:/Coq/ZArith/Zmin/Zmin_plus.con
cic:/Coq/ZArith/Zmisc/iter.con
cic:/Coq/ZArith/Zmisc/iter_nat.con
cic:/Coq/ZArith/Zmisc/iter_nat_invariant.con
cic:/Coq/ZArith/Zmisc/iter_nat_of_P.con
cic:/Coq/ZArith/Zmisc/iter_nat_plus.con
cic:/Coq/ZArith/Zmisc/iter_pos.con
cic:/Coq/ZArith/Zmisc/iter_pos_invariant.con
cic:/Coq/ZArith/Zmisc/iter_pos_plus.con
cic:/Coq/ZArith/Znat/Zpos_eq_Z_of_nat_o_nat_of_P.con
cic:/Coq/ZArith/Znat/inj_S.con
cic:/Coq/ZArith/Znat/inj_eq.con
cic:/Coq/ZArith/Znat/inj_ge.con
cic:/Coq/ZArith/Znat/inj_gt.con
cic:/Coq/ZArith/Znat/inj_le.con
cic:/Coq/ZArith/Znat/inj_lt.con
cic:/Coq/ZArith/Znat/inj_minus1.con
cic:/Coq/ZArith/Znat/inj_minus2.con
cic:/Coq/ZArith/Znat/inj_mult.con
cic:/Coq/ZArith/Znat/inj_neq.con
cic:/Coq/ZArith/Znat/inj_plus.con
cic:/Coq/ZArith/Znat/intro_Z.con
cic:/Coq/ZArith/Znat/neq.con
cic:/Coq/ZArith/Znumtheory/Bezout_ind.con
cic:/Coq/ZArith/Znumtheory/Euclid_ind.con
cic:/Coq/ZArith/Znumtheory/Euclid_rec.con
cic:/Coq/ZArith/Znumtheory/Euclid_rect.con
cic:/Coq/ZArith/Znumtheory/Gauss.con
cic:/Coq/ZArith/Znumtheory/Zdivide_0.con
cic:/Coq/ZArith/Znumtheory/Zdivide_1.con
cic:/Coq/ZArith/Znumtheory/Zdivide_1_subproof.con
cic:/Coq/ZArith/Znumtheory/Zdivide_1_subproof0.con
cic:/Coq/ZArith/Znumtheory/Zdivide_1_subproof1.con
cic:/Coq/ZArith/Znumtheory/Zdivide_antisym.con
cic:/Coq/ZArith/Znumtheory/Zdivide_bounds.con
cic:/Coq/ZArith/Znumtheory/Zdivide_bounds_subproof.con
cic:/Coq/ZArith/Znumtheory/Zdivide_bounds_subproof0.con
cic:/Coq/ZArith/Znumtheory/Zdivide_bounds_subproof1.con
cic:/Coq/ZArith/Znumtheory/Zdivide_bounds_subproof2.con
cic:/Coq/ZArith/Znumtheory/Zdivide_dec.con
cic:/Coq/ZArith/Znumtheory/Zdivide_dec_subproof.con
cic:/Coq/ZArith/Znumtheory/Zdivide_dec_subproof0.con
cic:/Coq/ZArith/Znumtheory/Zdivide_factor_l.con
cic:/Coq/ZArith/Znumtheory/Zdivide_factor_r.con
cic:/Coq/ZArith/Znumtheory/Zdivide_ind.con
cic:/Coq/ZArith/Znumtheory/Zdivide_minus_l.con
cic:/Coq/ZArith/Znumtheory/Zdivide_mod.con
cic:/Coq/ZArith/Znumtheory/Zdivide_mult_l.con
cic:/Coq/ZArith/Znumtheory/Zdivide_mult_r.con
cic:/Coq/ZArith/Znumtheory/Zdivide_opp_l.con
cic:/Coq/ZArith/Znumtheory/Zdivide_opp_l_rev.con
cic:/Coq/ZArith/Znumtheory/Zdivide_opp_r.con
cic:/Coq/ZArith/Znumtheory/Zdivide_opp_r_rev.con
cic:/Coq/ZArith/Znumtheory/Zdivide_plus_r.con
cic:/Coq/ZArith/Znumtheory/Zdivide_refl.con
cic:/Coq/ZArith/Znumtheory/Zgcd.con
cic:/Coq/ZArith/Znumtheory/Zgcd_is_gcd.con
cic:/Coq/ZArith/Znumtheory/Zgcd_is_pos.con
cic:/Coq/ZArith/Znumtheory/Zgcd_pos.con
cic:/Coq/ZArith/Znumtheory/Zgcd_pos_subproof.con
cic:/Coq/ZArith/Znumtheory/Zgcd_pos_subproof0.con
cic:/Coq/ZArith/Znumtheory/Zgcd_spec.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_0.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_bezout.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_for_euclid.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_for_euclid2.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_ind.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_minus.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_mult.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_opp.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_rec.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_rect.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_rel_prime.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_rel_prime_subproof.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_rel_prime_subproof0.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_rel_prime_subproof1.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_sym.con
cic:/Coq/ZArith/Znumtheory/Zis_gcd_uniqueness_apart_sign.con
cic:/Coq/ZArith/Znumtheory/Zmod_divide.con
cic:/Coq/ZArith/Znumtheory/Zmult_divide_compat_l.con
cic:/Coq/ZArith/Znumtheory/Zmult_divide_compat_r.con
cic:/Coq/ZArith/Znumtheory/Zmult_one.con
cic:/Coq/ZArith/Znumtheory/Zone_divide.con
cic:/Coq/ZArith/Znumtheory/bezout_rel_prime.con
cic:/Coq/ZArith/Znumtheory/euclid.con
cic:/Coq/ZArith/Znumtheory/euclid_rec.con
cic:/Coq/ZArith/Znumtheory/euclid_subproof.con
cic:/Coq/ZArith/Znumtheory/euclid_subproof0.con
cic:/Coq/ZArith/Znumtheory/euclid_subproof1.con
cic:/Coq/ZArith/Znumtheory/euclid_subproof2.con
cic:/Coq/ZArith/Znumtheory/prime_divisors.con
cic:/Coq/ZArith/Znumtheory/prime_divisors_subproof.con
cic:/Coq/ZArith/Znumtheory/prime_divisors_subproof0.con
cic:/Coq/ZArith/Znumtheory/prime_divisors_subproof1.con
cic:/Coq/ZArith/Znumtheory/prime_divisors_subproof2.con
cic:/Coq/ZArith/Znumtheory/prime_divisors_subproof3.con
cic:/Coq/ZArith/Znumtheory/prime_divisors_subproof4.con
cic:/Coq/ZArith/Znumtheory/prime_divisors_subproof5.con
cic:/Coq/ZArith/Znumtheory/prime_ind.con
cic:/Coq/ZArith/Znumtheory/prime_mult.con
cic:/Coq/ZArith/Znumtheory/prime_rec.con
cic:/Coq/ZArith/Znumtheory/prime_rect.con
cic:/Coq/ZArith/Znumtheory/prime_rel_prime.con
cic:/Coq/ZArith/Znumtheory/rel_prime.con
cic:/Coq/ZArith/Znumtheory/rel_prime_bezout.con
cic:/Coq/ZArith/Znumtheory/rel_prime_cross_prod.con
cic:/Coq/ZArith/Znumtheory/rel_prime_cross_prod_subproof.con
cic:/Coq/ZArith/Znumtheory/rel_prime_mult.con
cic:/Coq/ZArith/Zorder/Zeq_le.con
cic:/Coq/ZArith/Zorder/Zeq_plus_swap.con
cic:/Coq/ZArith/Zorder/Zge_iff_le.con
cic:/Coq/ZArith/Zorder/Zge_le.con
cic:/Coq/ZArith/Zorder/Zge_trans.con
cic:/Coq/ZArith/Zorder/Zge_trans_succ.con
cic:/Coq/ZArith/Zorder/Zgt_0_le_0_pred.con
cic:/Coq/ZArith/Zorder/Zgt_asym.con
cic:/Coq/ZArith/Zorder/Zgt_iff_lt.con
cic:/Coq/ZArith/Zorder/Zgt_irrefl.con
cic:/Coq/ZArith/Zorder/Zgt_le_succ.con
cic:/Coq/ZArith/Zorder/Zgt_le_trans.con
cic:/Coq/ZArith/Zorder/Zgt_lt.con
cic:/Coq/ZArith/Zorder/Zgt_not_le.con
cic:/Coq/ZArith/Zorder/Zgt_pos_0.con
cic:/Coq/ZArith/Zorder/Zgt_square_simpl.con
cic:/Coq/ZArith/Zorder/Zgt_succ.con
cic:/Coq/ZArith/Zorder/Zgt_succ_gt_or_eq.con
cic:/Coq/ZArith/Zorder/Zgt_succ_le.con
cic:/Coq/ZArith/Zorder/Zgt_succ_pred.con
cic:/Coq/ZArith/Zorder/Zgt_trans.con
cic:/Coq/ZArith/Zorder/Zle_0_1.con
cic:/Coq/ZArith/Zorder/Zle_0_nat.con
cic:/Coq/ZArith/Zorder/Zle_0_pos.con
cic:/Coq/ZArith/Zorder/Zle_antisym.con
cic:/Coq/ZArith/Zorder/Zle_ge.con
cic:/Coq/ZArith/Zorder/Zle_gt_trans.con
cic:/Coq/ZArith/Zorder/Zle_le_succ.con
cic:/Coq/ZArith/Zorder/Zle_lt_or_eq.con
cic:/Coq/ZArith/Zorder/Zle_lt_succ.con
cic:/Coq/ZArith/Zorder/Zle_lt_trans.con
cic:/Coq/ZArith/Zorder/Zle_neg_pos.con
cic:/Coq/ZArith/Zorder/Zle_not_gt.con
cic:/Coq/ZArith/Zorder/Zle_not_lt.con
cic:/Coq/ZArith/Zorder/Zle_or_lt.con
cic:/Coq/ZArith/Zorder/Zle_plus_swap.con
cic:/Coq/ZArith/Zorder/Zle_pred.con
cic:/Coq/ZArith/Zorder/Zle_refl.con
cic:/Coq/ZArith/Zorder/Zle_succ.con
cic:/Coq/ZArith/Zorder/Zle_succ_le.con
cic:/Coq/ZArith/Zorder/Zle_trans.con
cic:/Coq/ZArith/Zorder/Zlt_0_1.con
cic:/Coq/ZArith/Zorder/Zlt_0_le_0_pred.con
cic:/Coq/ZArith/Zorder/Zlt_O_minus_lt.con
cic:/Coq/ZArith/Zorder/Zlt_asym.con
cic:/Coq/ZArith/Zorder/Zlt_gt.con
cic:/Coq/ZArith/Zorder/Zlt_gt_succ.con
cic:/Coq/ZArith/Zorder/Zlt_irrefl.con
cic:/Coq/ZArith/Zorder/Zlt_le_succ.con
cic:/Coq/ZArith/Zorder/Zlt_le_trans.con
cic:/Coq/ZArith/Zorder/Zlt_le_weak.con
cic:/Coq/ZArith/Zorder/Zlt_lt_succ.con
cic:/Coq/ZArith/Zorder/Zlt_minus_simpl_swap.con
cic:/Coq/ZArith/Zorder/Zlt_neg_0.con
cic:/Coq/ZArith/Zorder/Zlt_not_eq.con
cic:/Coq/ZArith/Zorder/Zlt_not_le.con
cic:/Coq/ZArith/Zorder/Zlt_plus_swap.con
cic:/Coq/ZArith/Zorder/Zlt_pred.con
cic:/Coq/ZArith/Zorder/Zlt_square_simpl.con
cic:/Coq/ZArith/Zorder/Zlt_succ.con
cic:/Coq/ZArith/Zorder/Zlt_succ_gt.con
cic:/Coq/ZArith/Zorder/Zlt_succ_le.con
cic:/Coq/ZArith/Zorder/Zlt_succ_pred.con
cic:/Coq/ZArith/Zorder/Zlt_trans.con
cic:/Coq/ZArith/Zorder/Zmult_ge_compat.con
cic:/Coq/ZArith/Zorder/Zmult_ge_compat_l.con
cic:/Coq/ZArith/Zorder/Zmult_ge_compat_r.con
cic:/Coq/ZArith/Zorder/Zmult_ge_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_compat.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_le_0_compat.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_le_compat_r.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_0_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_compat_l.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_compat_r.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_gt_0_reg_l.con
cic:/Coq/ZArith/Zorder/Zmult_gt_compat_l.con
cic:/Coq/ZArith/Zorder/Zmult_gt_compat_r.con
cic:/Coq/ZArith/Zorder/Zmult_gt_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con
cic:/Coq/ZArith/Zorder/Zmult_le_0_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_le_compat.con
cic:/Coq/ZArith/Zorder/Zmult_le_compat_l.con
cic:/Coq/ZArith/Zorder/Zmult_le_compat_r.con
cic:/Coq/ZArith/Zorder/Zmult_le_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_lt_0_le_compat_r.con
cic:/Coq/ZArith/Zorder/Zmult_lt_0_le_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_lt_0_reg_r.con
cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con
cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con
cic:/Coq/ZArith/Zorder/Zmult_lt_compat_r.con
cic:/Coq/ZArith/Zorder/Zmult_lt_reg_r.con
cic:/Coq/ZArith/Zorder/Znot_ge_lt.con
cic:/Coq/ZArith/Zorder/Znot_gt_le.con
cic:/Coq/ZArith/Zorder/Znot_le_gt.con
cic:/Coq/ZArith/Zorder/Znot_le_succ.con
cic:/Coq/ZArith/Zorder/Znot_lt_ge.con
cic:/Coq/ZArith/Zorder/Zplus_gt_compat_l.con
cic:/Coq/ZArith/Zorder/Zplus_gt_compat_r.con
cic:/Coq/ZArith/Zorder/Zplus_gt_reg_l.con
cic:/Coq/ZArith/Zorder/Zplus_gt_reg_r.con
cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con
cic:/Coq/ZArith/Zorder/Zplus_le_compat.con
cic:/Coq/ZArith/Zorder/Zplus_le_compat_l.con
cic:/Coq/ZArith/Zorder/Zplus_le_compat_r.con
cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con
cic:/Coq/ZArith/Zorder/Zplus_le_reg_l.con
cic:/Coq/ZArith/Zorder/Zplus_le_reg_r.con
cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con
cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con
cic:/Coq/ZArith/Zorder/Zplus_lt_compat_r.con
cic:/Coq/ZArith/Zorder/Zplus_lt_le_compat.con
cic:/Coq/ZArith/Zorder/Zplus_lt_reg_l.con
cic:/Coq/ZArith/Zorder/Zplus_lt_reg_r.con
cic:/Coq/ZArith/Zorder/Zsucc_gt_compat.con
cic:/Coq/ZArith/Zorder/Zsucc_gt_reg.con
cic:/Coq/ZArith/Zorder/Zsucc_le_compat.con
cic:/Coq/ZArith/Zorder/Zsucc_le_reg.con
cic:/Coq/ZArith/Zorder/Zsucc_lt_compat.con
cic:/Coq/ZArith/Zorder/Zsucc_lt_reg.con
cic:/Coq/ZArith/Zorder/Ztrichotomy.con
cic:/Coq/ZArith/Zorder/Ztrichotomy_inf.con
cic:/Coq/ZArith/Zorder/dec_Zge.con
cic:/Coq/ZArith/Zorder/dec_Zgt.con
cic:/Coq/ZArith/Zorder/dec_Zle.con
cic:/Coq/ZArith/Zorder/dec_Zlt.con
cic:/Coq/ZArith/Zorder/dec_Zne.con
cic:/Coq/ZArith/Zorder/dec_eq.con
cic:/Coq/ZArith/Zorder/not_Zeq.con
cic:/Coq/ZArith/Zpower/Zdiv_rest.con
cic:/Coq/ZArith/Zpower/Zdiv_rest_aux.con
cic:/Coq/ZArith/Zpower/Zdiv_rest_correct.con
cic:/Coq/ZArith/Zpower/Zdiv_rest_correct1.con
cic:/Coq/ZArith/Zpower/Zdiv_rest_correct2.con
cic:/Coq/ZArith/Zpower/Zdiv_rest_proofs_ind.con
cic:/Coq/ZArith/Zpower/Zdiv_rest_proofs_rec.con
cic:/Coq/ZArith/Zpower/Zdiv_rest_proofs_rect.con
cic:/Coq/ZArith/Zpower/Zlt_lt_double.con
cic:/Coq/ZArith/Zpower/Zpower.con
cic:/Coq/ZArith/Zpower/Zpower_exp.con
cic:/Coq/ZArith/Zpower/Zpower_nat.con
cic:/Coq/ZArith/Zpower/Zpower_nat_is_exp.con
cic:/Coq/ZArith/Zpower/Zpower_pos.con
cic:/Coq/ZArith/Zpower/Zpower_pos_is_exp.con
cic:/Coq/ZArith/Zpower/Zpower_pos_nat.con
cic:/Coq/ZArith/Zpower/shift.con
cic:/Coq/ZArith/Zpower/shift_nat.con
cic:/Coq/ZArith/Zpower/shift_nat_correct.con
cic:/Coq/ZArith/Zpower/shift_nat_plus.con
cic:/Coq/ZArith/Zpower/shift_pos.con
cic:/Coq/ZArith/Zpower/shift_pos_correct.con
cic:/Coq/ZArith/Zpower/shift_pos_nat.con
cic:/Coq/ZArith/Zpower/two_p.con
cic:/Coq/ZArith/Zpower/two_p_S.con
cic:/Coq/ZArith/Zpower/two_p_gt_ZERO.con
cic:/Coq/ZArith/Zpower/two_p_is_exp.con
cic:/Coq/ZArith/Zpower/two_p_pred.con
cic:/Coq/ZArith/Zpower/two_power_nat.con
cic:/Coq/ZArith/Zpower/two_power_nat_S.con
cic:/Coq/ZArith/Zpower/two_power_nat_correct.con
cic:/Coq/ZArith/Zpower/two_power_pos.con
cic:/Coq/ZArith/Zpower/two_power_pos_correct.con
cic:/Coq/ZArith/Zpower/two_power_pos_is_exp.con
cic:/Coq/ZArith/Zpower/two_power_pos_nat.con
cic:/Coq/ZArith/Zsqrt/Zsqrt.con
cic:/Coq/ZArith/Zsqrt/Zsqrt_interval.con
cic:/Coq/ZArith/Zsqrt/Zsqrt_plain.con
cic:/Coq/ZArith/Zsqrt/sqrt_data_ind.con
cic:/Coq/ZArith/Zsqrt/sqrt_data_rec.con
cic:/Coq/ZArith/Zsqrt/sqrt_data_rect.con
cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
cic:/Coq/ZArith/Zwf/Zwf.con
cic:/Coq/ZArith/Zwf/Zwf_up.con
cic:/Coq/ZArith/Zwf/Zwf_up_well_founded.con
cic:/Coq/ZArith/Zwf/Zwf_well_founded.con
cic:/Coq/ZArith/auxiliary/Zegal_left.con
cic:/Coq/ZArith/auxiliary/Zge_left.con
cic:/Coq/ZArith/auxiliary/Zgt_left.con
cic:/Coq/ZArith/auxiliary/Zgt_left_gt.con
cic:/Coq/ZArith/auxiliary/Zgt_left_rev.con
cic:/Coq/ZArith/auxiliary/Zle_left.con
cic:/Coq/ZArith/auxiliary/Zle_left_rev.con
cic:/Coq/ZArith/auxiliary/Zle_mult_approx.con
cic:/Coq/ZArith/auxiliary/Zlt_left.con
cic:/Coq/ZArith/auxiliary/Zlt_left_lt.con
cic:/Coq/ZArith/auxiliary/Zlt_left_rev.con
cic:/Coq/ZArith/auxiliary/Zmult_le_approx.con
cic:/Coq/ZArith/auxiliary/Zne_left.con
cic:/Coq/ZArith/auxiliary/Zred_factor0.con
cic:/Coq/ZArith/auxiliary/Zred_factor1.con
cic:/Coq/ZArith/auxiliary/Zred_factor2.con
cic:/Coq/ZArith/auxiliary/Zred_factor3.con
cic:/Coq/ZArith/auxiliary/Zred_factor4.con
cic:/Coq/ZArith/auxiliary/Zred_factor5.con
cic:/Coq/ZArith/auxiliary/Zred_factor6.con
cic:/Coq/field/Field_Compl/appT.con
cic:/Coq/field/Field_Compl/assoc_2nd.con
cic:/Coq/field/Field_Compl/field_rel_option_ind.con
cic:/Coq/field/Field_Compl/field_rel_option_rec.con
cic:/Coq/field/Field_Compl/field_rel_option_rect.con
cic:/Coq/field/Field_Compl/fstT.con
cic:/Coq/field/Field_Compl/listT_ind.con
cic:/Coq/field/Field_Compl/listT_rec.con
cic:/Coq/field/Field_Compl/listT_rect.con
cic:/Coq/field/Field_Compl/mem.con
cic:/Coq/field/Field_Compl/prodT_ind.con
cic:/Coq/field/Field_Compl/prodT_rec.con
cic:/Coq/field/Field_Compl/prodT_rect.con
cic:/Coq/field/Field_Compl/sndT.con
cic:/Coq/field/Field_Theory/A.con
cic:/Coq/field/Field_Theory/Adiv.con
cic:/Coq/field/Field_Theory/Aeq.con
cic:/Coq/field/Field_Theory/Ainv.con
cic:/Coq/field/Field_Theory/AinvT_r.con
cic:/Coq/field/Field_Theory/Aminus.con
cic:/Coq/field/Field_Theory/Amult.con
cic:/Coq/field/Field_Theory/AmultT_1l.con
cic:/Coq/field/Field_Theory/AmultT_1r.con
cic:/Coq/field/Field_Theory/AmultT_AplusT_distr.con
cic:/Coq/field/Field_Theory/AmultT_Ol.con
cic:/Coq/field/Field_Theory/AmultT_Or.con
cic:/Coq/field/Field_Theory/AmultT_assoc.con
cic:/Coq/field/Field_Theory/AmultT_sym.con
cic:/Coq/field/Field_Theory/Aone.con
cic:/Coq/field/Field_Theory/Aopp.con
cic:/Coq/field/Field_Theory/Aplus.con
cic:/Coq/field/Field_Theory/AplusT_AoppT_r.con
cic:/Coq/field/Field_Theory/AplusT_Ol.con
cic:/Coq/field/Field_Theory/AplusT_assoc.con
cic:/Coq/field/Field_Theory/AplusT_sym.con
cic:/Coq/field/Field_Theory/Azero.con
cic:/Coq/field/Field_Theory/ExprA_ind.con
cic:/Coq/field/Field_Theory/ExprA_rec.con
cic:/Coq/field/Field_Theory/ExprA_rect.con
cic:/Coq/field/Field_Theory/Field_Theory_ind.con
cic:/Coq/field/Field_Theory/Field_Theory_rec.con
cic:/Coq/field/Field_Theory/Field_Theory_rect.con
cic:/Coq/field/Field_Theory/RT.con
cic:/Coq/field/Field_Theory/Rmult_neq_0_reg.con
cic:/Coq/field/Field_Theory/Th_inv_def.con
cic:/Coq/field/Field_Theory/assoc.con
cic:/Coq/field/Field_Theory/assoc_correct.con
cic:/Coq/field/Field_Theory/assoc_mult.con
cic:/Coq/field/Field_Theory/assoc_mult_correct.con
cic:/Coq/field/Field_Theory/assoc_mult_correct1.con
cic:/Coq/field/Field_Theory/assoc_plus_correct.con
cic:/Coq/field/Field_Theory/distrib.con
cic:/Coq/field/Field_Theory/distrib_EAopp.con
cic:/Coq/field/Field_Theory/distrib_correct.con
cic:/Coq/field/Field_Theory/distrib_main.con
cic:/Coq/field/Field_Theory/distrib_mult_left.con
cic:/Coq/field/Field_Theory/distrib_mult_left_correct.con
cic:/Coq/field/Field_Theory/distrib_mult_right.con
cic:/Coq/field/Field_Theory/distrib_mult_right_correct.con
cic:/Coq/field/Field_Theory/eqExprA.con
cic:/Coq/field/Field_Theory/eqExprA_O.con
cic:/Coq/field/Field_Theory/eq_nat_dec.con
cic:/Coq/field/Field_Theory/interp_ExprA.con
cic:/Coq/field/Field_Theory/inverse_correct.con
cic:/Coq/field/Field_Theory/inverse_simplif.con
cic:/Coq/field/Field_Theory/merge_mult.con
cic:/Coq/field/Field_Theory/merge_mult_correct.con
cic:/Coq/field/Field_Theory/merge_mult_correct1.con
cic:/Coq/field/Field_Theory/merge_plus.con
cic:/Coq/field/Field_Theory/merge_plus_correct.con
cic:/Coq/field/Field_Theory/merge_plus_correct1.con
cic:/Coq/field/Field_Theory/monom_remove.con
cic:/Coq/field/Field_Theory/monom_remove_correct.con
cic:/Coq/field/Field_Theory/monom_simplif.con
cic:/Coq/field/Field_Theory/monom_simplif_correct.con
cic:/Coq/field/Field_Theory/monom_simplif_rem.con
cic:/Coq/field/Field_Theory/monom_simplif_rem_correct.con
cic:/Coq/field/Field_Theory/mult_eq.con
cic:/Coq/field/Field_Theory/mult_of_list.con
cic:/Coq/field/Field_Theory/multiply.con
cic:/Coq/field/Field_Theory/multiply_aux.con
cic:/Coq/field/Field_Theory/multiply_aux_correct.con
cic:/Coq/field/Field_Theory/multiply_correct.con
cic:/Coq/field/Field_Theory/r_AmultT_mult.con
cic:/Coq/field/Field_Theory/r_AplusT_plus.con
cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con
cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con
cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con
cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con
cic:/Coq/fourier/Fourier_util/Rfourier_le.con
cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con
cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con
cic:/Coq/fourier/Fourier_util/Rfourier_lt.con
cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con
cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con
cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con
cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con
cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con
cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con
cic:/Coq/fourier/Fourier_util/Rle_not_lt.con
cic:/Coq/fourier/Fourier_util/Rle_zero_1.con
cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con
cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con
cic:/Coq/fourier/Fourier_util/Rlt_not_le.con
cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con
cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con
cic:/Coq/fourier/Fourier_util/Rnot_le_le.con
cic:/Coq/fourier/Fourier_util/Rnot_lt0.con
cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con
cic:/Coq/omega/OmegaLemmas/OMEGA1.con
cic:/Coq/omega/OmegaLemmas/OMEGA10.con
cic:/Coq/omega/OmegaLemmas/OMEGA11.con
cic:/Coq/omega/OmegaLemmas/OMEGA12.con
cic:/Coq/omega/OmegaLemmas/OMEGA13.con
cic:/Coq/omega/OmegaLemmas/OMEGA14.con
cic:/Coq/omega/OmegaLemmas/OMEGA15.con
cic:/Coq/omega/OmegaLemmas/OMEGA16.con
cic:/Coq/omega/OmegaLemmas/OMEGA17.con
cic:/Coq/omega/OmegaLemmas/OMEGA18.con
cic:/Coq/omega/OmegaLemmas/OMEGA19.con
cic:/Coq/omega/OmegaLemmas/OMEGA2.con
cic:/Coq/omega/OmegaLemmas/OMEGA20.con
cic:/Coq/omega/OmegaLemmas/OMEGA3.con
cic:/Coq/omega/OmegaLemmas/OMEGA4.con
cic:/Coq/omega/OmegaLemmas/OMEGA5.con
cic:/Coq/omega/OmegaLemmas/OMEGA6.con
cic:/Coq/omega/OmegaLemmas/OMEGA7.con
cic:/Coq/omega/OmegaLemmas/OMEGA8.con
cic:/Coq/omega/OmegaLemmas/OMEGA9.con
cic:/Coq/omega/OmegaLemmas/fast_OMEGA10.con
cic:/Coq/omega/OmegaLemmas/fast_OMEGA11.con
cic:/Coq/omega/OmegaLemmas/fast_OMEGA12.con
cic:/Coq/omega/OmegaLemmas/fast_OMEGA13.con
cic:/Coq/omega/OmegaLemmas/fast_OMEGA14.con
cic:/Coq/omega/OmegaLemmas/fast_OMEGA15.con
cic:/Coq/omega/OmegaLemmas/fast_OMEGA16.con
cic:/Coq/omega/OmegaLemmas/fast_Zmult_Zopp_left.con
cic:/Coq/omega/OmegaLemmas/fast_Zmult_assoc_r.con
cic:/Coq/omega/OmegaLemmas/fast_Zmult_plus_distr.con
cic:/Coq/omega/OmegaLemmas/fast_Zmult_sym.con
cic:/Coq/omega/OmegaLemmas/fast_Zopp_Zmult_r.con
cic:/Coq/omega/OmegaLemmas/fast_Zopp_Zopp.con
cic:/Coq/omega/OmegaLemmas/fast_Zopp_Zplus.con
cic:/Coq/omega/OmegaLemmas/fast_Zopp_one.con
cic:/Coq/omega/OmegaLemmas/fast_Zplus_assoc_l.con
cic:/Coq/omega/OmegaLemmas/fast_Zplus_assoc_r.con
cic:/Coq/omega/OmegaLemmas/fast_Zplus_permute.con
cic:/Coq/omega/OmegaLemmas/fast_Zplus_sym.con
cic:/Coq/omega/OmegaLemmas/fast_Zred_factor0.con
cic:/Coq/omega/OmegaLemmas/fast_Zred_factor1.con
cic:/Coq/omega/OmegaLemmas/fast_Zred_factor2.con
cic:/Coq/omega/OmegaLemmas/fast_Zred_factor3.con
cic:/Coq/omega/OmegaLemmas/fast_Zred_factor4.con
cic:/Coq/omega/OmegaLemmas/fast_Zred_factor5.con
cic:/Coq/omega/OmegaLemmas/fast_Zred_factor6.con
cic:/Coq/omega/OmegaLemmas/new_var.con
cic:/Coq/ring/ArithRing/NatTheory.con
cic:/Coq/ring/ArithRing/S_to_plus_one.con
cic:/Coq/ring/ArithRing/nateq.con
cic:/Coq/ring/ArithRing/nateq_prop.con
cic:/Coq/ring/NArithRing/NTheory.con
cic:/Coq/ring/NArithRing/Neq.con
cic:/Coq/ring/NArithRing/Neq_prop.con
cic:/Coq/ring/Quote/index_eq.con
cic:/Coq/ring/Quote/index_eq_prop.con
cic:/Coq/ring/Quote/index_ind.con
cic:/Coq/ring/Quote/index_lt.con
cic:/Coq/ring/Quote/index_rec.con
cic:/Coq/ring/Quote/index_rect.con
cic:/Coq/ring/Quote/varmap_find.con
cic:/Coq/ring/Quote/varmap_ind.con
cic:/Coq/ring/Quote/varmap_rec.con
cic:/Coq/ring/Quote/varmap_rect.con
cic:/Coq/ring/Ring/BoolTheory.con
cic:/Coq/ring/Ring_abstract/abstract_sum_ind.con
cic:/Coq/ring/Ring_abstract/abstract_sum_merge.con
cic:/Coq/ring/Ring_abstract/abstract_sum_merge_ok.con
cic:/Coq/ring/Ring_abstract/abstract_sum_prod.con
cic:/Coq/ring/Ring_abstract/abstract_sum_prod_ok.con
cic:/Coq/ring/Ring_abstract/abstract_sum_rec.con
cic:/Coq/ring/Ring_abstract/abstract_sum_rect.con
cic:/Coq/ring/Ring_abstract/abstract_sum_scalar.con
cic:/Coq/ring/Ring_abstract/abstract_sum_scalar_ok.con
cic:/Coq/ring/Ring_abstract/abstract_varlist_insert.con
cic:/Coq/ring/Ring_abstract/abstract_varlist_insert_ok.con
cic:/Coq/ring/Ring_abstract/apolynomial_ind.con
cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con
cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con
cic:/Coq/ring/Ring_abstract/apolynomial_rec.con
cic:/Coq/ring/Ring_abstract/apolynomial_rect.con
cic:/Coq/ring/Ring_abstract/aspolynomial_ind.con
cic:/Coq/ring/Ring_abstract/aspolynomial_normalize.con
cic:/Coq/ring/Ring_abstract/aspolynomial_normalize_ok.con
cic:/Coq/ring/Ring_abstract/aspolynomial_rec.con
cic:/Coq/ring/Ring_abstract/aspolynomial_rect.con
cic:/Coq/ring/Ring_abstract/iacs_aux.con
cic:/Coq/ring/Ring_abstract/iacs_aux_ok.con
cic:/Coq/ring/Ring_abstract/interp_acs.con
cic:/Coq/ring/Ring_abstract/interp_ap.con
cic:/Coq/ring/Ring_abstract/interp_asp.con
cic:/Coq/ring/Ring_abstract/interp_sacs.con
cic:/Coq/ring/Ring_abstract/isacs_aux.con
cic:/Coq/ring/Ring_abstract/isacs_aux_ok.con
cic:/Coq/ring/Ring_abstract/minus_sum_scalar.con
cic:/Coq/ring/Ring_abstract/minus_sum_scalar_ok.con
cic:/Coq/ring/Ring_abstract/minus_varlist_insert.con
cic:/Coq/ring/Ring_abstract/minus_varlist_insert_ok.con
cic:/Coq/ring/Ring_abstract/plus_sum_scalar.con
cic:/Coq/ring/Ring_abstract/plus_sum_scalar_ok.con
cic:/Coq/ring/Ring_abstract/plus_varlist_insert.con
cic:/Coq/ring/Ring_abstract/plus_varlist_insert_ok.con
cic:/Coq/ring/Ring_abstract/signed_sum_ind.con
cic:/Coq/ring/Ring_abstract/signed_sum_merge.con
cic:/Coq/ring/Ring_abstract/signed_sum_merge_ok.con
cic:/Coq/ring/Ring_abstract/signed_sum_opp.con
cic:/Coq/ring/Ring_abstract/signed_sum_opp_ok.con
cic:/Coq/ring/Ring_abstract/signed_sum_prod.con
cic:/Coq/ring/Ring_abstract/signed_sum_prod_ok.con
cic:/Coq/ring/Ring_abstract/signed_sum_rec.con
cic:/Coq/ring/Ring_abstract/signed_sum_rect.con
cic:/Coq/ring/Ring_normalize/canonical_sum_ind.con
cic:/Coq/ring/Ring_normalize/canonical_sum_merge.con
cic:/Coq/ring/Ring_normalize/canonical_sum_merge_ok.con
cic:/Coq/ring/Ring_normalize/canonical_sum_prod.con
cic:/Coq/ring/Ring_normalize/canonical_sum_prod_ok.con
cic:/Coq/ring/Ring_normalize/canonical_sum_rec.con
cic:/Coq/ring/Ring_normalize/canonical_sum_rect.con
cic:/Coq/ring/Ring_normalize/canonical_sum_scalar.con
cic:/Coq/ring/Ring_normalize/canonical_sum_scalar2.con
cic:/Coq/ring/Ring_normalize/canonical_sum_scalar2_ok.con
cic:/Coq/ring/Ring_normalize/canonical_sum_scalar3.con
cic:/Coq/ring/Ring_normalize/canonical_sum_scalar3_ok.con
cic:/Coq/ring/Ring_normalize/canonical_sum_scalar_ok.con
cic:/Coq/ring/Ring_normalize/canonical_sum_simplify.con
cic:/Coq/ring/Ring_normalize/canonical_sum_simplify_ok.con
cic:/Coq/ring/Ring_normalize/ics_aux.con
cic:/Coq/ring/Ring_normalize/ics_aux_ok.con
cic:/Coq/ring/Ring_normalize/index_eq_prop.con
cic:/Coq/ring/Ring_normalize/interp_cs.con
cic:/Coq/ring/Ring_normalize/interp_m.con
cic:/Coq/ring/Ring_normalize/interp_m_ok.con
cic:/Coq/ring/Ring_normalize/interp_p.con
cic:/Coq/ring/Ring_normalize/interp_sp.con
cic:/Coq/ring/Ring_normalize/interp_var.con
cic:/Coq/ring/Ring_normalize/interp_vl.con
cic:/Coq/ring/Ring_normalize/ivl_aux.con
cic:/Coq/ring/Ring_normalize/ivl_aux_ok.con
cic:/Coq/ring/Ring_normalize/monom_insert.con
cic:/Coq/ring/Ring_normalize/monom_insert_ok.con
cic:/Coq/ring/Ring_normalize/polynomial_ind.con
cic:/Coq/ring/Ring_normalize/polynomial_normalize.con
cic:/Coq/ring/Ring_normalize/polynomial_normalize_ok.con
cic:/Coq/ring/Ring_normalize/polynomial_rec.con
cic:/Coq/ring/Ring_normalize/polynomial_rect.con
cic:/Coq/ring/Ring_normalize/polynomial_simplify.con
cic:/Coq/ring/Ring_normalize/polynomial_simplify_ok.con
cic:/Coq/ring/Ring_normalize/spolynomial_ind.con
cic:/Coq/ring/Ring_normalize/spolynomial_normalize.con
cic:/Coq/ring/Ring_normalize/spolynomial_normalize_ok.con
cic:/Coq/ring/Ring_normalize/spolynomial_of.con
cic:/Coq/ring/Ring_normalize/spolynomial_of_ok.con
cic:/Coq/ring/Ring_normalize/spolynomial_rec.con
cic:/Coq/ring/Ring_normalize/spolynomial_rect.con
cic:/Coq/ring/Ring_normalize/spolynomial_simplify.con
cic:/Coq/ring/Ring_normalize/spolynomial_simplify_ok.con
cic:/Coq/ring/Ring_normalize/varlist_eq.con
cic:/Coq/ring/Ring_normalize/varlist_eq_prop.con
cic:/Coq/ring/Ring_normalize/varlist_ind.con
cic:/Coq/ring/Ring_normalize/varlist_insert.con
cic:/Coq/ring/Ring_normalize/varlist_insert_ok.con
cic:/Coq/ring/Ring_normalize/varlist_lt.con
cic:/Coq/ring/Ring_normalize/varlist_merge.con
cic:/Coq/ring/Ring_normalize/varlist_merge_ok.con
cic:/Coq/ring/Ring_normalize/varlist_rec.con
cic:/Coq/ring/Ring_normalize/varlist_rect.con
cic:/Coq/ring/Ring_theory/Ring_Theory_ind.con
cic:/Coq/ring/Ring_theory/Ring_Theory_rec.con
cic:/Coq/ring/Ring_theory/Ring_Theory_rect.con
cic:/Coq/ring/Ring_theory/SR_distr_left.con
cic:/Coq/ring/Ring_theory/SR_distr_left2.con
cic:/Coq/ring/Ring_theory/SR_distr_right.con
cic:/Coq/ring/Ring_theory/SR_distr_right2.con
cic:/Coq/ring/Ring_theory/SR_eq_prop.con
cic:/Coq/ring/Ring_theory/SR_mult_assoc.con
cic:/Coq/ring/Ring_theory/SR_mult_assoc2.con
cic:/Coq/ring/Ring_theory/SR_mult_comm.con
cic:/Coq/ring/Ring_theory/SR_mult_one_left.con
cic:/Coq/ring/Ring_theory/SR_mult_one_left2.con
cic:/Coq/ring/Ring_theory/SR_mult_one_right.con
cic:/Coq/ring/Ring_theory/SR_mult_one_right2.con
cic:/Coq/ring/Ring_theory/SR_mult_permute.con
cic:/Coq/ring/Ring_theory/SR_mult_zero_left.con
cic:/Coq/ring/Ring_theory/SR_mult_zero_left2.con
cic:/Coq/ring/Ring_theory/SR_mult_zero_right.con
cic:/Coq/ring/Ring_theory/SR_mult_zero_right2.con
cic:/Coq/ring/Ring_theory/SR_plus_assoc.con
cic:/Coq/ring/Ring_theory/SR_plus_assoc2.con
cic:/Coq/ring/Ring_theory/SR_plus_comm.con
cic:/Coq/ring/Ring_theory/SR_plus_permute.con
cic:/Coq/ring/Ring_theory/SR_plus_reg_left.con
cic:/Coq/ring/Ring_theory/SR_plus_reg_right.con
cic:/Coq/ring/Ring_theory/SR_plus_zero_left.con
cic:/Coq/ring/Ring_theory/SR_plus_zero_left2.con
cic:/Coq/ring/Ring_theory/SR_plus_zero_right.con
cic:/Coq/ring/Ring_theory/SR_plus_zero_right2.con
cic:/Coq/ring/Ring_theory/Semi_Ring_Theory_ind.con
cic:/Coq/ring/Ring_theory/Semi_Ring_Theory_of.con
cic:/Coq/ring/Ring_theory/Semi_Ring_Theory_rec.con
cic:/Coq/ring/Ring_theory/Semi_Ring_Theory_rect.con
cic:/Coq/ring/Ring_theory/Th_distr_left.con
cic:/Coq/ring/Ring_theory/Th_distr_left2.con
cic:/Coq/ring/Ring_theory/Th_distr_right.con
cic:/Coq/ring/Ring_theory/Th_distr_right2.con
cic:/Coq/ring/Ring_theory/Th_eq_prop.con
cic:/Coq/ring/Ring_theory/Th_mult_assoc.con
cic:/Coq/ring/Ring_theory/Th_mult_assoc2.con
cic:/Coq/ring/Ring_theory/Th_mult_one_left.con
cic:/Coq/ring/Ring_theory/Th_mult_one_left2.con
cic:/Coq/ring/Ring_theory/Th_mult_one_right.con
cic:/Coq/ring/Ring_theory/Th_mult_one_right2.con
cic:/Coq/ring/Ring_theory/Th_mult_opp_opp.con
cic:/Coq/ring/Ring_theory/Th_mult_opp_opp2.con
cic:/Coq/ring/Ring_theory/Th_mult_permute.con
cic:/Coq/ring/Ring_theory/Th_mult_sym.con
cic:/Coq/ring/Ring_theory/Th_mult_zero_left.con
cic:/Coq/ring/Ring_theory/Th_mult_zero_left2.con
cic:/Coq/ring/Ring_theory/Th_mult_zero_right.con
cic:/Coq/ring/Ring_theory/Th_mult_zero_right2.con
cic:/Coq/ring/Ring_theory/Th_opp_def.con
cic:/Coq/ring/Ring_theory/Th_opp_def2.con
cic:/Coq/ring/Ring_theory/Th_opp_mult_left.con
cic:/Coq/ring/Ring_theory/Th_opp_mult_left2.con
cic:/Coq/ring/Ring_theory/Th_opp_mult_right.con
cic:/Coq/ring/Ring_theory/Th_opp_mult_right2.con
cic:/Coq/ring/Ring_theory/Th_opp_opp.con
cic:/Coq/ring/Ring_theory/Th_opp_opp2.con
cic:/Coq/ring/Ring_theory/Th_opp_zero.con
cic:/Coq/ring/Ring_theory/Th_plus_assoc.con
cic:/Coq/ring/Ring_theory/Th_plus_assoc2.con
cic:/Coq/ring/Ring_theory/Th_plus_comm.con
cic:/Coq/ring/Ring_theory/Th_plus_opp_opp.con
cic:/Coq/ring/Ring_theory/Th_plus_permute.con
cic:/Coq/ring/Ring_theory/Th_plus_permute_opp.con
cic:/Coq/ring/Ring_theory/Th_plus_reg_left.con
cic:/Coq/ring/Ring_theory/Th_plus_reg_right.con
cic:/Coq/ring/Ring_theory/Th_plus_zero_left.con
cic:/Coq/ring/Ring_theory/Th_plus_zero_left2.con
cic:/Coq/ring/Ring_theory/Th_plus_zero_right.con
cic:/Coq/ring/Ring_theory/Th_plus_zero_right2.con
cic:/Coq/ring/Ring_theory/aux1.con
cic:/Coq/ring/Ring_theory/aux2.con
cic:/Coq/ring/Setoid_ring_normalize/Amult_ext.con
cic:/Coq/ring/Setoid_ring_normalize/Aopp_ext.con
cic:/Coq/ring/Setoid_ring_normalize/Aplus_ext.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_ind.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_merge.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_merge_ok.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_prod.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_prod_ok.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_rec.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_rect.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_scalar.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_scalar2.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_scalar2_ok.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_scalar3.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_scalar3_ok.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_scalar_ok.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_simplify.con
cic:/Coq/ring/Setoid_ring_normalize/canonical_sum_simplify_ok.con
cic:/Coq/ring/Setoid_ring_normalize/ics_aux.con
cic:/Coq/ring/Setoid_ring_normalize/ics_aux_ok.con
cic:/Coq/ring/Setoid_ring_normalize/index_eq_prop.con
cic:/Coq/ring/Setoid_ring_normalize/interp_m.con
cic:/Coq/ring/Setoid_ring_normalize/interp_m_ok.con
cic:/Coq/ring/Setoid_ring_normalize/interp_setcs.con
cic:/Coq/ring/Setoid_ring_normalize/interp_setp.con
cic:/Coq/ring/Setoid_ring_normalize/interp_setsp.con
cic:/Coq/ring/Setoid_ring_normalize/interp_var.con
cic:/Coq/ring/Setoid_ring_normalize/interp_vl.con
cic:/Coq/ring/Setoid_ring_normalize/ivl_aux.con
cic:/Coq/ring/Setoid_ring_normalize/ivl_aux_ok.con
cic:/Coq/ring/Setoid_ring_normalize/monom_insert.con
cic:/Coq/ring/Setoid_ring_normalize/monom_insert_ok.con
cic:/Coq/ring/Setoid_ring_normalize/setoid_eq_ext1.con
cic:/Coq/ring/Setoid_ring_normalize/setoid_eq_ext2.con
cic:/Coq/ring/Setoid_ring_normalize/setpolynomial_ind.con
cic:/Coq/ring/Setoid_ring_normalize/setpolynomial_normalize.con
cic:/Coq/ring/Setoid_ring_normalize/setpolynomial_normalize_ok.con
cic:/Coq/ring/Setoid_ring_normalize/setpolynomial_rec.con
cic:/Coq/ring/Setoid_ring_normalize/setpolynomial_rect.con
cic:/Coq/ring/Setoid_ring_normalize/setpolynomial_simplify.con
cic:/Coq/ring/Setoid_ring_normalize/setpolynomial_simplify_ok.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_ind.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_normalize.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_normalize_ok.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_of.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_of_ok.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_rec.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_rect.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_simplify.con
cic:/Coq/ring/Setoid_ring_normalize/setspolynomial_simplify_ok.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_eq.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_eq_prop.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_ind.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_insert.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_insert_ok.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_lt.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_merge.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_merge_ok.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_rec.con
cic:/Coq/ring/Setoid_ring_normalize/varlist_rect.con
cic:/Coq/ring/Setoid_ring_theory/Amult_ext.con
cic:/Coq/ring/Setoid_ring_theory/Aopp_ext.con
cic:/Coq/ring/Setoid_ring_theory/Aplus_ext.con
cic:/Coq/ring/Setoid_ring_theory/SSR_distr_left.con
cic:/Coq/ring/Setoid_ring_theory/SSR_distr_left2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_distr_right.con
cic:/Coq/ring/Setoid_ring_theory/SSR_distr_right2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_eq_prop.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_assoc.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_assoc2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_comm.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_one_left.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_one_left2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_one_right.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_one_right2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_permute.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_zero_left.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_zero_left2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_zero_right.con
cic:/Coq/ring/Setoid_ring_theory/SSR_mult_zero_right2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_assoc.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_assoc2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_comm.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_permute.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_reg_left.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_reg_right.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_zero_left.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_zero_left2.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_zero_right.con
cic:/Coq/ring/Setoid_ring_theory/SSR_plus_zero_right2.con
cic:/Coq/ring/Setoid_ring_theory/STh_distr_left.con
cic:/Coq/ring/Setoid_ring_theory/STh_distr_left2.con
cic:/Coq/ring/Setoid_ring_theory/STh_distr_right.con
cic:/Coq/ring/Setoid_ring_theory/STh_distr_right2.con
cic:/Coq/ring/Setoid_ring_theory/STh_eq_prop.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_assoc.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_assoc2.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_one_left.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_one_left2.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_one_right.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_one_right2.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_opp_opp.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_opp_opp2.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_permute.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_sym.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_zero_left.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_zero_left2.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_zero_right.con
cic:/Coq/ring/Setoid_ring_theory/STh_mult_zero_right2.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_def.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_def2.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_mult_left.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_mult_left2.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_mult_right.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_mult_right2.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_opp.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_opp2.con
cic:/Coq/ring/Setoid_ring_theory/STh_opp_zero.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_assoc.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_assoc2.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_comm.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_opp_opp.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_permute.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_permute_opp.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_reg_left.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_reg_right.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_zero_left.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_zero_left2.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_zero_right.con
cic:/Coq/ring/Setoid_ring_theory/STh_plus_zero_right2.con
cic:/Coq/ring/Setoid_ring_theory/Saux1.con
cic:/Coq/ring/Setoid_ring_theory/Saux2.con
cic:/Coq/ring/Setoid_ring_theory/Semi_Setoid_Ring_Theory_ind.con
cic:/Coq/ring/Setoid_ring_theory/Semi_Setoid_Ring_Theory_of.con
cic:/Coq/ring/Setoid_ring_theory/Semi_Setoid_Ring_Theory_rec.con
cic:/Coq/ring/Setoid_ring_theory/Semi_Setoid_Ring_Theory_rect.con
cic:/Coq/ring/Setoid_ring_theory/Setoid_Ring_Theory_ind.con
cic:/Coq/ring/Setoid_ring_theory/Setoid_Ring_Theory_rec.con
cic:/Coq/ring/Setoid_ring_theory/Setoid_Ring_Theory_rect.con
cic:/Coq/ring/Setoid_ring_theory/setoid_eq_ext1.con
cic:/Coq/ring/Setoid_ring_theory/setoid_eq_ext2.con
cic:/Coq/ring/ZArithRing/ZTheory.con
cic:/Coq/ring/ZArithRing/Zeq.con
cic:/Coq/ring/ZArithRing/Zeq_prop.con
cic:/Coq/romega/ReflOmegaCore/PropList_ind.con
cic:/Coq/romega/ReflOmegaCore/PropList_rec.con
cic:/Coq/romega/ReflOmegaCore/PropList_rect.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA10.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA10_stable.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA11.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA11_stable.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA12.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA12_stable.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA13.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA13_stable.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA15.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA15_stable.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA16.con
cic:/Coq/romega/ReflOmegaCore/T_OMEGA16_stable.con
cic:/Coq/romega/ReflOmegaCore/Tminus_def.con
cic:/Coq/romega/ReflOmegaCore/Tminus_def_stable.con
cic:/Coq/romega/ReflOmegaCore/Tmult_assoc_r.con
cic:/Coq/romega/ReflOmegaCore/Tmult_assoc_r_stable.con
cic:/Coq/romega/ReflOmegaCore/Tmult_assoc_reduced.con
cic:/Coq/romega/ReflOmegaCore/Tmult_assoc_reduced_stable.con
cic:/Coq/romega/ReflOmegaCore/Tmult_opp_left.con
cic:/Coq/romega/ReflOmegaCore/Tmult_opp_left_stable.con
cic:/Coq/romega/ReflOmegaCore/Tmult_plus_distr.con
cic:/Coq/romega/ReflOmegaCore/Tmult_plus_distr_stable.con
cic:/Coq/romega/ReflOmegaCore/Tmult_sym.con
cic:/Coq/romega/ReflOmegaCore/Tmult_sym_stable.con
cic:/Coq/romega/ReflOmegaCore/Topp_mult_r.con
cic:/Coq/romega/ReflOmegaCore/Topp_mult_r_stable.con
cic:/Coq/romega/ReflOmegaCore/Topp_one.con
cic:/Coq/romega/ReflOmegaCore/Topp_one_stable.con
cic:/Coq/romega/ReflOmegaCore/Topp_opp.con
cic:/Coq/romega/ReflOmegaCore/Topp_opp_stable.con
cic:/Coq/romega/ReflOmegaCore/Topp_plus.con
cic:/Coq/romega/ReflOmegaCore/Topp_plus_stable.con
cic:/Coq/romega/ReflOmegaCore/Tplus_assoc_l.con
cic:/Coq/romega/ReflOmegaCore/Tplus_assoc_l_stable.con
cic:/Coq/romega/ReflOmegaCore/Tplus_assoc_r.con
cic:/Coq/romega/ReflOmegaCore/Tplus_assoc_r_stable.con
cic:/Coq/romega/ReflOmegaCore/Tplus_permute.con
cic:/Coq/romega/ReflOmegaCore/Tplus_permute_stable.con
cic:/Coq/romega/ReflOmegaCore/Tplus_sym.con
cic:/Coq/romega/ReflOmegaCore/Tplus_sym_stable.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor0.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor0_stable.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor1.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor1_stable.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor2.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor2_stable.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor3.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor3_stable.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor4.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor4_stable.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor5.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor5_stable.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor6.con
cic:/Coq/romega/ReflOmegaCore/Tred_factor6_stable.con
cic:/Coq/romega/ReflOmegaCore/Zlt_left_inv.con
cic:/Coq/romega/ReflOmegaCore/Zne_left_2.con
cic:/Coq/romega/ReflOmegaCore/absurd.con
cic:/Coq/romega/ReflOmegaCore/add_norm.con
cic:/Coq/romega/ReflOmegaCore/add_norm_stable.con
cic:/Coq/romega/ReflOmegaCore/append_goal.con
cic:/Coq/romega/ReflOmegaCore/append_valid.con
cic:/Coq/romega/ReflOmegaCore/apply_both.con
cic:/Coq/romega/ReflOmegaCore/apply_both_stable.con
cic:/Coq/romega/ReflOmegaCore/apply_left.con
cic:/Coq/romega/ReflOmegaCore/apply_left_stable.con
cic:/Coq/romega/ReflOmegaCore/apply_oper_1.con
cic:/Coq/romega/ReflOmegaCore/apply_oper_1_valid.con
cic:/Coq/romega/ReflOmegaCore/apply_oper_2.con
cic:/Coq/romega/ReflOmegaCore/apply_oper_2_valid.con
cic:/Coq/romega/ReflOmegaCore/apply_right.con
cic:/Coq/romega/ReflOmegaCore/apply_right_stable.con
cic:/Coq/romega/ReflOmegaCore/bool_ind2.con
cic:/Coq/romega/ReflOmegaCore/co_valid1.con
cic:/Coq/romega/ReflOmegaCore/compose_term_stable.con
cic:/Coq/romega/ReflOmegaCore/concl_to_hyp.con
cic:/Coq/romega/ReflOmegaCore/constant_neg.con
cic:/Coq/romega/ReflOmegaCore/constant_neg_valid.con
cic:/Coq/romega/ReflOmegaCore/constant_not_nul.con
cic:/Coq/romega/ReflOmegaCore/constant_not_nul_valid.con
cic:/Coq/romega/ReflOmegaCore/constant_nul.con
cic:/Coq/romega/ReflOmegaCore/constant_nul_valid.con
cic:/Coq/romega/ReflOmegaCore/contradiction.con
cic:/Coq/romega/ReflOmegaCore/contradiction_valid.con
cic:/Coq/romega/ReflOmegaCore/decidability.con
cic:/Coq/romega/ReflOmegaCore/decidable_correct.con
cic:/Coq/romega/ReflOmegaCore/decompose_solve.con
cic:/Coq/romega/ReflOmegaCore/decompose_solve_valid.con
cic:/Coq/romega/ReflOmegaCore/destructure_hyps.con
cic:/Coq/romega/ReflOmegaCore/destructure_hyps_valid.con
cic:/Coq/romega/ReflOmegaCore/direction_ind.con
cic:/Coq/romega/ReflOmegaCore/direction_rec.con
cic:/Coq/romega/ReflOmegaCore/direction_rect.con
cic:/Coq/romega/ReflOmegaCore/divide_and_approx.con
cic:/Coq/romega/ReflOmegaCore/divide_and_approx_valid.con
cic:/Coq/romega/ReflOmegaCore/do_concl_to_hyp.con
cic:/Coq/romega/ReflOmegaCore/do_normalize.con
cic:/Coq/romega/ReflOmegaCore/do_normalize_list.con
cic:/Coq/romega/ReflOmegaCore/do_normalize_list_valid.con
cic:/Coq/romega/ReflOmegaCore/do_normalize_valid.con
cic:/Coq/romega/ReflOmegaCore/do_omega.con
cic:/Coq/romega/ReflOmegaCore/do_reduce_lhyps.con
cic:/Coq/romega/ReflOmegaCore/e_step_ind.con
cic:/Coq/romega/ReflOmegaCore/e_step_rec.con
cic:/Coq/romega/ReflOmegaCore/e_step_rect.con
cic:/Coq/romega/ReflOmegaCore/eq_Z.con
cic:/Coq/romega/ReflOmegaCore/eq_Z_false.con
cic:/Coq/romega/ReflOmegaCore/eq_Z_true.con
cic:/Coq/romega/ReflOmegaCore/eq_nat.con
cic:/Coq/romega/ReflOmegaCore/eq_nat_false.con
cic:/Coq/romega/ReflOmegaCore/eq_nat_true.con
cic:/Coq/romega/ReflOmegaCore/eq_pos.con
cic:/Coq/romega/ReflOmegaCore/eq_pos_false.con
cic:/Coq/romega/ReflOmegaCore/eq_pos_true.con
cic:/Coq/romega/ReflOmegaCore/eq_term.con
cic:/Coq/romega/ReflOmegaCore/eq_term_false.con
cic:/Coq/romega/ReflOmegaCore/eq_term_true.con
cic:/Coq/romega/ReflOmegaCore/exact_divide.con
cic:/Coq/romega/ReflOmegaCore/exact_divide_valid.con
cic:/Coq/romega/ReflOmegaCore/execute_goal.con
cic:/Coq/romega/ReflOmegaCore/execute_omega.con
cic:/Coq/romega/ReflOmegaCore/extract_hyp_neg.con
cic:/Coq/romega/ReflOmegaCore/extract_hyp_pos.con
cic:/Coq/romega/ReflOmegaCore/extract_valid.con
cic:/Coq/romega/ReflOmegaCore/fusion.con
cic:/Coq/romega/ReflOmegaCore/fusion_cancel.con
cic:/Coq/romega/ReflOmegaCore/fusion_cancel_stable.con
cic:/Coq/romega/ReflOmegaCore/fusion_right.con
cic:/Coq/romega/ReflOmegaCore/fusion_stable.con
cic:/Coq/romega/ReflOmegaCore/goal_to_hyps.con
cic:/Coq/romega/ReflOmegaCore/goal_valid.con
cic:/Coq/romega/ReflOmegaCore/h_step_ind.con
cic:/Coq/romega/ReflOmegaCore/h_step_rec.con
cic:/Coq/romega/ReflOmegaCore/h_step_rect.con
cic:/Coq/romega/ReflOmegaCore/hyps_to_goal.con
cic:/Coq/romega/ReflOmegaCore/interp_full.con
cic:/Coq/romega/ReflOmegaCore/interp_full_false.con
cic:/Coq/romega/ReflOmegaCore/interp_full_goal.con
cic:/Coq/romega/ReflOmegaCore/interp_goal_concl.con
cic:/Coq/romega/ReflOmegaCore/interp_hyps.con
cic:/Coq/romega/ReflOmegaCore/interp_list_goal.con
cic:/Coq/romega/ReflOmegaCore/interp_list_hyps.con
cic:/Coq/romega/ReflOmegaCore/interp_proposition.con
cic:/Coq/romega/ReflOmegaCore/interp_term.con
cic:/Coq/romega/ReflOmegaCore/list_goal_to_hyps.con
cic:/Coq/romega/ReflOmegaCore/list_hyps_to_goal.con
cic:/Coq/romega/ReflOmegaCore/map_cons.con
cic:/Coq/romega/ReflOmegaCore/map_cons_val.con
cic:/Coq/romega/ReflOmegaCore/merge_eq.con
cic:/Coq/romega/ReflOmegaCore/merge_eq_valid.con
cic:/Coq/romega/ReflOmegaCore/move_right.con
cic:/Coq/romega/ReflOmegaCore/move_right_stable.con
cic:/Coq/romega/ReflOmegaCore/move_right_valid.con
cic:/Coq/romega/ReflOmegaCore/negate_contradict.con
cic:/Coq/romega/ReflOmegaCore/negate_contradict_inv.con
cic:/Coq/romega/ReflOmegaCore/negate_contradict_inv_valid.con
cic:/Coq/romega/ReflOmegaCore/negate_contradict_valid.con
cic:/Coq/romega/ReflOmegaCore/normalize_goal.con
cic:/Coq/romega/ReflOmegaCore/normalize_hyps.con
cic:/Coq/romega/ReflOmegaCore/normalize_hyps_goal.con
cic:/Coq/romega/ReflOmegaCore/normalize_hyps_valid.con
cic:/Coq/romega/ReflOmegaCore/not_exact_divide.con
cic:/Coq/romega/ReflOmegaCore/not_exact_divide_valid.con
cic:/Coq/romega/ReflOmegaCore/nthProp.con
cic:/Coq/romega/ReflOmegaCore/nth_hyps.con
cic:/Coq/romega/ReflOmegaCore/nth_valid.con
cic:/Coq/romega/ReflOmegaCore/omega_tactic.con
cic:/Coq/romega/ReflOmegaCore/omega_valid.con
cic:/Coq/romega/ReflOmegaCore/p_apply_left.con
cic:/Coq/romega/ReflOmegaCore/p_apply_left_stable.con
cic:/Coq/romega/ReflOmegaCore/p_apply_right.con
cic:/Coq/romega/ReflOmegaCore/p_apply_right_stable.con
cic:/Coq/romega/ReflOmegaCore/p_invert.con
cic:/Coq/romega/ReflOmegaCore/p_invert_stable.con
cic:/Coq/romega/ReflOmegaCore/p_rewrite.con
cic:/Coq/romega/ReflOmegaCore/p_rewrite_stable.con
cic:/Coq/romega/ReflOmegaCore/p_step_ind.con
cic:/Coq/romega/ReflOmegaCore/p_step_rec.con
cic:/Coq/romega/ReflOmegaCore/p_step_rect.con
cic:/Coq/romega/ReflOmegaCore/prop_stable.con
cic:/Coq/romega/ReflOmegaCore/proposition_ind.con
cic:/Coq/romega/ReflOmegaCore/proposition_rec.con
cic:/Coq/romega/ReflOmegaCore/proposition_rect.con
cic:/Coq/romega/ReflOmegaCore/reduce.con
cic:/Coq/romega/ReflOmegaCore/reduce_lhyps.con
cic:/Coq/romega/ReflOmegaCore/reduce_lhyps_valid.con
cic:/Coq/romega/ReflOmegaCore/reduce_stable.con
cic:/Coq/romega/ReflOmegaCore/relation_ind2.con
cic:/Coq/romega/ReflOmegaCore/rewrite.con
cic:/Coq/romega/ReflOmegaCore/rewrite_stable.con
cic:/Coq/romega/ReflOmegaCore/scalar_norm.con
cic:/Coq/romega/ReflOmegaCore/scalar_norm_add.con
cic:/Coq/romega/ReflOmegaCore/scalar_norm_add_stable.con
cic:/Coq/romega/ReflOmegaCore/scalar_norm_stable.con
cic:/Coq/romega/ReflOmegaCore/split_ineq.con
cic:/Coq/romega/ReflOmegaCore/split_ineq_valid.con
cic:/Coq/romega/ReflOmegaCore/state.con
cic:/Coq/romega/ReflOmegaCore/state_valid.con
cic:/Coq/romega/ReflOmegaCore/step_ind.con
cic:/Coq/romega/ReflOmegaCore/step_rec.con
cic:/Coq/romega/ReflOmegaCore/step_rect.con
cic:/Coq/romega/ReflOmegaCore/sum.con
cic:/Coq/romega/ReflOmegaCore/sum1.con
cic:/Coq/romega/ReflOmegaCore/sum2.con
cic:/Coq/romega/ReflOmegaCore/sum3.con
cic:/Coq/romega/ReflOmegaCore/sum4.con
cic:/Coq/romega/ReflOmegaCore/sum5.con
cic:/Coq/romega/ReflOmegaCore/sum_valid.con
cic:/Coq/romega/ReflOmegaCore/t_fusion_ind.con
cic:/Coq/romega/ReflOmegaCore/t_fusion_rec.con
cic:/Coq/romega/ReflOmegaCore/t_fusion_rect.con
cic:/Coq/romega/ReflOmegaCore/t_omega_ind.con
cic:/Coq/romega/ReflOmegaCore/t_omega_rec.con
cic:/Coq/romega/ReflOmegaCore/t_omega_rect.con
cic:/Coq/romega/ReflOmegaCore/term_ind.con
cic:/Coq/romega/ReflOmegaCore/term_rec.con
cic:/Coq/romega/ReflOmegaCore/term_rect.con
cic:/Coq/romega/ReflOmegaCore/term_stable.con
cic:/Coq/romega/ReflOmegaCore/to_contradict.con
cic:/Coq/romega/ReflOmegaCore/to_contradict_valid.con
cic:/Coq/romega/ReflOmegaCore/valid1.con
cic:/Coq/romega/ReflOmegaCore/valid2.con
cic:/Coq/romega/ReflOmegaCore/valid_goal.con
cic:/Coq/romega/ReflOmegaCore/valid_hyps.con
cic:/Coq/romega/ReflOmegaCore/valid_lhyps.con
cic:/Coq/romega/ReflOmegaCore/valid_list_goal.con
cic:/Coq/romega/ReflOmegaCore/valid_list_hyps.con