L (lemma)
land_spec [in land_spec]
law_cosines [in law_cosines]
lb_to_glb [in lb_to_glb]
ldiff_spec [in ldiff_spec]
leA_Tree_Leaf [in leA_Tree_Leaf]
leA_Tree_Node [in leA_Tree_Node]
leb_complete_conv [in leb_complete_conv]
leb_implb [in leb_implb]
leb_compare [in leb_compare]
leb_le [in leb_le]
leb_correct [in leb_correct]
leb_correct_conv [in leb_correct_conv]
leb_iff [in leb_iff]
leb_refl [in leb_refl]
leb_complete [in leb_complete]
leb_iff_conv [in leb_iff_conv]
leftinv_is_rightinv [in leftinv_is_rightinv]
leftinv_is_rightinv_interv [in leftinv_is_rightinv_interv]
left_prefix [in left_prefix]
lel_tail [in lel_tail]
lel_cons [in lel_cons]
lel_trans [in lel_trans]
lel_nil [in lel_nil]
lel_cons_cons [in lel_cons_cons]
lel_refl [in lel_refl]
Lemma1 [in Lemma1]
lemma1 [in lemma1]
lemma2 [in lemma2]
length_pos_lt [in length_pos_lt]
less_than_empty [in less_than_empty]
less_than_singleton [in less_than_singleton]
le_or_lt [in le_or_lt]
le_not_gt [in le_not_gt]
le_minus [in le_minus]
le_plus_trans [in le_plus_trans]
le_plus_r [in le_plus_r]
le_le_S_eq [in le_le_S_eq]
le_lt_or_eq [in le_lt_or_eq]
le_elim_rel [in le_elim_rel]
le_gt_trans [in le_gt_trans]
le_trans [in le_trans]
le_trans [in le_trans]
le_IZR [in le_IZR]
le_n_2n [in le_n_2n]
le_n_Sn [in le_n_Sn]
le_IZR_R1 [in le_IZR_R1]
le_S_gt [in le_S_gt]
le_epsilon [in le_epsilon]
le_n_S [in le_n_S]
le_Sn_n [in le_Sn_n]
le_dec [in le_dec]
le_dec [in le_dec]
le_Order [in le_Order]
le_0_n [in le_0_n]
le_double [in le_double]
le_Sn_0 [in le_Sn_0]
le_0_IZR [in le_0_IZR]
le_pred [in le_pred]
le_pred [in le_pred]
le_lt_n_Sm [in le_lt_n_Sm]
le_plus_minus_r [in le_plus_minus_r]
le_unique [in le_unique]
le_antisym [in le_antisym]
le_antisym [in le_antisym]
le_not_lt [in le_not_lt]
le_total_order [in le_total_order]
le_n_0_eq [in le_n_0_eq]
le_INR [in le_INR]
le_plus_minus [in le_plus_minus]
le_ni_le [in le_ni_le]
le_decide [in le_decide]
le_gt_S [in le_gt_S]
le_minusni_n [in le_minusni_n]
le_pred_n [in le_pred_n]
le_S_n [in le_S_n]
le_S_n [in le_S_n]
le_lt_trans [in le_lt_trans]
le_plus_l [in le_plus_l]
le_lt_or_eq_iff [in le_lt_or_eq_iff]
le_Pmult_nat [in le_Pmult_nat]
le_reflexive [in le_reflexive]
le_refl [in le_refl]
le_Sn_le [in le_Sn_le]
limit_Ropp [in limit_Ropp]
limit_minus [in limit_minus]
limit_inv [in limit_inv]
limit_free [in limit_free]
limit_comp [in limit_comp]
limit_mul [in limit_mul]
limit_plus [in limit_plus]
limit1_ext [in limit1_ext]
limit1_imp [in limit1_imp]
lim_x [in lim_x]
list_to_heap [in list_to_heap]
list_contents_app [in list_contents_app]
list_eq_dec [in list_eq_dec]
ln_continue [in ln_continue]
ln_inv [in ln_inv]
ln_1 [in ln_1]
ln_exp [in ln_exp]
ln_exists1 [in ln_exists1]
ln_mult [in ln_mult]
ln_lt_inv [in ln_lt_inv]
ln_lt_2 [in ln_lt_2]
ln_exists [in ln_exists]
ln_Rinv [in ln_Rinv]
ln_increasing [in ln_increasing]
log_sup_le_Slog_inf [in log_sup_le_Slog_inf]
log_inf_bounded [in log_inf_bounded]
log_sup_correct1 [in log_sup_correct1]
log_sup_shift_nat [in log_sup_shift_nat]
log_inf_correct [in log_inf_correct]
log_near_correct1 [in log_near_correct1]
log_sup_correct2 [in log_sup_correct2]
log_inf_le_log_sup [in log_inf_le_log_sup]
log_near_correct2 [in log_near_correct2]
log_sup_log_inf [in log_sup_log_inf]
log_inf_shift_nat [in log_inf_shift_nat]
log2_spec [in log2_spec]
log2_nonpos [in log2_nonpos]
log2_iter_spec [in log2_iter_spec]
lor_spec [in lor_spec]
low_trans [in low_trans]
ltb_lt [in ltb_lt]
ltl_unit [in ltl_unit]
lt_INR [in lt_INR]
lt_le_weak [in lt_le_weak]
lt_S [in lt_S]
lt_wB_wwB [in lt_wB_wwB]
lt_plus_trans [in lt_plus_trans]
lt_irrefl [in lt_irrefl]
lt_minus_O_lt [in lt_minus_O_lt]
lt_minus [in lt_minus]
lt_1_INR [in lt_1_INR]
lt_0_wB [in lt_0_wB]
lt_n_S [in lt_n_S]
lt_dec [in lt_dec]
lt_0_Sn [in lt_0_Sn]
lt_not_le [in lt_not_le]
lt_0_wwB [in lt_0_wwB]
lt_wf_rec [in lt_wf_rec]
lt_le_trans [in lt_le_trans]
lt_div2 [in lt_div2]
lt_pred [in lt_pred]
lt_0_INR [in lt_0_INR]
lt_wf [in lt_wf]
lt_0_IZR [in lt_0_IZR]
lt_le_S [in lt_le_S]
lt_IZR [in lt_IZR]
lt_pred_n_n [in lt_pred_n_n]
lt_wf_double_rec [in lt_wf_double_rec]
lt_O_fact [in lt_O_fact]
lt_wf_rec1 [in lt_wf_rec1]
lt_trans [in lt_trans]
lt_0_neq [in lt_0_neq]
lt_asym [in lt_asym]
lt_O_minus_lt [in lt_O_minus_lt]
lt_n_Sn [in lt_n_Sn]
lt_wf_ind [in lt_wf_ind]
lt_n_Sm_le [in lt_n_Sm_le]
lt_n_0 [in lt_n_0]
lt_S_n [in lt_S_n]
lt_wf_double_ind [in lt_wf_double_ind]
lxor_spec [in lxor_spec]
L_sanity [in L_sanity]
L1 [in L1]
l2i_i2l [in l2i_i2l]