G
g [definition, in g]
Gauss [lemma, in Gauss]
gcd [definition, in gcd]
gcd [definition, in gcd]
Gcd [module, in Gcd]
gcd_gt [definition, in gcd_gt]
gcd_cont [definition, in gcd_cont]
gcd_greatest [lemma, in gcd_greatest]
gcd_divide_r [lemma, in gcd_divide_r]
gcd_divide [lemma, in gcd_divide]
gcd_divide_l [lemma, in gcd_divide_l]
Gcd.gcd [axiom, in gcd]
gcd31 [definition, in gcd31]
ge [definition, in ge]
gen [lemma, in gen]
GENDIVN1 [section, in GENDIVN1]
GENDIVN1.DIVAUX [section, in DIVAUX]
GENDIVN1.DIVAUX.b2p [variable, in b2p]
GENDIVN1.DIVAUX.b2p_le [variable, in b2p_le]
GENDIVN1.DIVAUX.p [variable, in p]
GENDIVN1.DIVAUX.p_bounded [variable, in p_bounded]
GENDIVN1.spec_add_mul_div [variable, in spec_add_mul_div]
GENDIVN1.spec_div21 [variable, in spec_div21]
GENDIVN1.spec_WW [variable, in spec_WW]
GENDIVN1.spec_head0 [variable, in spec_head0]
GENDIVN1.spec_compare [variable, in spec_compare]
GENDIVN1.spec_to_Z [variable, in spec_to_Z]
GENDIVN1.spec_sub [variable, in spec_sub]
GENDIVN1.spec_w_zdigits [variable, in spec_w_zdigits]
GENDIVN1.spec_0 [variable, in spec_0]
GENDIVN1.w [variable, in w]
GENDIVN1.w_div21 [variable, in w_div21]
GENDIVN1.w_digits [variable, in w_digits]
GENDIVN1.w_head0 [variable, in w_head0]
GENDIVN1.w_sub [variable, in w_sub]
GENDIVN1.w_compare [variable, in w_compare]
GENDIVN1.w_to_Z [variable, in w_to_Z]
GENDIVN1.w_WW [variable, in w_WW]
GENDIVN1.w_add_mul_div [variable, in w_add_mul_div]
GENDIVN1.w_0 [variable, in w_0]
GENDIVN1.w_zdigits [variable, in w_zdigits]
[! _ | _ !] [notation, in ::'[!'_x_'|'_x_'!]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
generalized_excluded_middle [definition, in generalized_excluded_middle]
Generalized_induction_on_finite_sets [lemma, in Generalized_induction_on_finite_sets]
Generic [section, in Generic]
Generic [section, in Generic]
GenericAbs [module, in GenericAbs]
GenericAbs.abs [definition, in abs]
GenericAbs.abs_eq [lemma, in abs_eq]
GenericAbs.abs_neq [lemma, in abs_neq]
GenericMinMax [module, in GenericMinMax]
GenericMinMax [library]
GenericMinMax.ge_not_lt [lemma, in ge_not_lt]
GenericMinMax.max [definition, in max]
GenericMinMax.max_r [lemma, in max_r]
GenericMinMax.max_l [lemma, in max_l]
GenericMinMax.min [definition, in min]
GenericMinMax.min_r [lemma, in min_r]
GenericMinMax.min_l [lemma, in min_l]
GenericSgn [module, in GenericSgn]
GenericSgn.sgn [definition, in sgn]
GenericSgn.sgn_pos [lemma, in sgn_pos]
GenericSgn.sgn_null [lemma, in sgn_null]
GenericSgn.sgn_neg [lemma, in sgn_neg]
Generic.U [variable, in U]
Generic.U [variable, in U]
gen_st [definition, in gen_st]
get [definition, in get]
get_height_correct [lemma, in get_height_correct]
get_height [definition, in get_height]
get_correct [lemma, in get_correct]
get_low [definition, in get_low]
ge_dec [lemma, in ge_dec]
glb [definition, in glb]
Glb [inductive, in Glb]
Glb_definition [constructor, in Glb_definition]
gmax [definition, in gmax]
gmin [definition, in gmin]
GodelDummett [definition, in GodelDummett]
Godel_Dummett_weak_excluded_middle [lemma, in Godel_Dummett_weak_excluded_middle]
Godel_Dummett_iff_right_distr_implication_over_disjunction [lemma, in Godel_Dummett_iff_right_distr_implication_over_disjunction]
GP_finite [lemma, in GP_finite]
GP_infinite [lemma, in GP_infinite]
growing_cv [lemma, in growing_cv]
growing_prop [lemma, in growing_prop]
growing_ineq [lemma, in growing_ineq]
Gt [constructor, in Gt]
gt [definition, in gt]
GT [constructor, in GT]
Gt [library]
gtof [definition, in gtof]
gt_le_trans [lemma, in gt_le_trans]
gt_S_n [lemma, in gt_S_n]
gt_irrefl [lemma, in gt_irrefl]
gt_dec [lemma, in gt_dec]
gt_not_le [lemma, in gt_not_le]
gt_n_S [lemma, in gt_n_S]
gt_O_eq [abbreviation, in gt_O_eq]
gt_asym [lemma, in gt_asym]
gt_0_eq [lemma, in gt_0_eq]
gt_Sn_n [lemma, in gt_Sn_n]
gt_wf_rec [lemma, in gt_wf_rec]
gt_S [lemma, in gt_S]
gt_pred [lemma, in gt_pred]
gt_eq_gt_dec [definition, in gt_eq_gt_dec]
gt_trans [lemma, in gt_trans]
gt_S_le [lemma, in gt_S_le]
gt_wf_ind [lemma, in gt_wf_ind]
gt_le_S [lemma, in gt_le_S]
gt_trans_S [lemma, in gt_trans_S]
gt_Sn_O [lemma, in gt_Sn_O]
GuardedFunctionalChoice [abbreviation, in GuardedFunctionalChoice]
GuardedFunctionalChoice_on [definition, in GuardedFunctionalChoice_on]
GuardedFunctionalRelReification [abbreviation, in GuardedFunctionalRelReification]
GuardedFunctionalRelReification_on [definition, in GuardedFunctionalRelReification_on]
GuardedRelationalChoice [abbreviation, in GuardedRelationalChoice]
GuardedRelationalChoice_on [definition, in GuardedRelationalChoice_on]
guarded_fun_choice_imp_fun_choice [lemma, in guarded_fun_choice_imp_fun_choice]
guarded_rel_choice_imp_rel_choice [lemma, in guarded_rel_choice_imp_rel_choice]
guarded_iff_omniscient_rel_choice [lemma, in guarded_iff_omniscient_rel_choice]
guarded_fun_choice_imp_indep_of_general_premises [lemma, in guarded_fun_choice_imp_indep_of_general_premises]
guarded_rel_choice [lemma, in guarded_rel_choice]
guarded_iff_omniscient_fun_choice [lemma, in guarded_iff_omniscient_fun_choice]
G_aux [lemma, in G_aux]