Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (390 entries) |

Tactic Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (6 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (277 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (54 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (44 entries) |

add_un_add [lemma, in nat_morphism2]

add_un_add [lemma, in nat_morphism]

already_normalized_ok [lemma, in top_sqrt]

auxiliary_for_sqrt_goals1 [lemma, in sqrt_goals2]

aux_shift_1 [definition, in specifications]

aux_1 [lemma, in sqrt_prog]

aux_10 [lemma, in sqrt_prog]

aux_11 [lemma, in sqrt_prog]

aux_12 [lemma, in sqrt_prog]

aux_13 [lemma, in sqrt_prog]

aux_2 [lemma, in sqrt_prog]

aux_3 [lemma, in sqrt_prog]

aux_4 [lemma, in sqrt_prog]

aux_5 [lemma, in sqrt_prog]

aux_6 [lemma, in sqrt_prog]

aux_7 [lemma, in sqrt_prog]

aux_8 [lemma, in sqrt_prog]

aux_9 [lemma, in sqrt_prog]

A1 [lemma, in Zextensions]

A1' [lemma, in lemmas]

A2 [lemma, in Zextensions]

b [definition, in top_sqrt]

beta [definition, in top_sqrt]

beta [definition, in specifications]

betaGt0 [lemma, in mpn_complements]

betaGt0 [lemma, in top_sqrt]

betaGt1 [axiom, in specifications]

betaGt2 [lemma, in mpn_complements]

betaMultipleTwo [lemma, in top_sqrt]

beta' [axiom, in specifications]

between_0_1 [lemma, in sqrt_prog]

between_0_1' [lemma, in sqrt_prog]

bool2nat [definition, in sqrt_prog]

bool2Z [definition, in sqrt_prog]

borrow_bound [lemma, in mpn_complements]

borrow_positive [lemma, in mpn_complements]

borrow_positive' [lemma, in mpn_complements]

bound [axiom, in specifications]

bPos [lemma, in fun]

bPowPos [lemma, in fun]

build_aux_thms [module]

ceildivPos [lemma, in div2]

ceildiv2 [definition, in div2]

ceildiv2' [definition, in div2]

ceildiv2_aux_lemma [lemma, in div2]

ceildiv2_characteristic [lemma, in div2]

ceildiv2_eq [lemma, in div2]

compute_POS [tactic definition, in compute_POS]

compute_POS [module]

correct_goals [module]

correct_goal1 [lemma, in correct_goals]

correct_goal2 [lemma, in correct_goals]

correct_goal3 [lemma, in correct_goals]

correct_goal4 [lemma, in correct_goals]

correct_goal5 [lemma, in correct_goals]

correct_goal6 [lemma, in correct_goals]

correct_goal7 [lemma, in correct_goals]

correct_result [module]

c_decompose [constructor, in fun_aux]

c_sqrt [constructor, in sqrtrembase]

divDefBreakdown2 [tactic definition, in proof_sqrt]

divDefBreakdown3 [tactic definition, in proof_sqrt]

divDefBreakdown4 [tactic definition, in proof_sqrt]

division_step [module]

divltle2 [lemma, in top_misc]

divrem' [definition, in fun]

div2 [module]

div2' [definition, in sqrt_prog]

div2_double_le [lemma, in sqrt_prog]

div2_floordiv2_equal [lemma, in sqrt_prog]

div2_le [lemma, in sqrt_prog]

div2_minus [lemma, in sqrt_prog]

div2_minus' [lemma, in sqrt_prog]

div2_minus_lt [lemma, in sqrt_prog]

div2_mult2 [lemma, in sqrt_prog]

div2_nn_l [lemma, in sqrt_prog]

div2_odd [lemma, in sqrt_prog]

div2_thm1 [lemma, in top_misc]

div2_thm2 [lemma, in top_misc]

div2_thm3 [lemma, in top_misc]

div2_thm4 [lemma, in top_misc]

div2_01 [lemma, in top_misc]

div_goals [module]

div_goals10 [module]

div_goals11 [module]

div_goals12 [module]

div_goals13 [module]

div_goals2 [module]

div_goals3 [module]

div_goals4 [module]

div_goals5 [module]

div_goals6 [module]

div_goals7 [module]

div_goals8 [module]

div_goals9 [module]

div_goal1 [lemma, in div_goals]

div_goal10 [lemma, in div_goals10]

div_goal11 [lemma, in div_goals11]

div_goal12 [lemma, in div_goals12]

div_goal13 [lemma, in div_goals13]

div_goal2 [lemma, in div_goals2]

div_goal3 [lemma, in div_goals3]

div_goal4 [lemma, in div_goals4]

div_goal5 [lemma, in div_goals5]

div_goal6 [lemma, in div_goals6]

div_goal7 [lemma, in div_goals7]

div_goal8 [lemma, in div_goals8]

div_goal9 [lemma, in div_goals9]

div_rem_uniqueness [lemma, in top_sqrt]

easy_thm2 [lemma, in top_sqrt]

exponentbMulipleFour [lemma, in fun_aux]

exponentbMulipleFour [lemma, in fun]

floordiv2_ge [lemma, in div2]

floordiv2_le_ceildiv2 [lemma, in div2]

former_prop4 [lemma, in proof_sqrt]

fun [module]

fun_aux [module]

f' [definition, in specifications]

Hhalfpos [lemma, in proof_sqrt]

Hhalf_easy [lemma, in sqrt_prog]

Hpos [lemma, in proof_sqrt]

implies_normalized [lemma, in top_sqrt]

implies_normalized_N1 [lemma, in top_sqrt]

Impnumber_access [lemma, in mpn_complements]

Impnumber_between [lemma, in mpn_complements]

Impnumber_bound [lemma, in mpn_complements]

Impnumber_decompose [lemma, in mpn_complements]

Impnumber_unchanged [lemma, in mpn_complements]

Impnumber_unchanged_bis [lemma, in mpn_complements]

inj_minus_div2 [lemma, in sqrt_prog]

isEvenOrOdd [definition, in specifications]

IsNormalized [definition, in proof_sqrt]

I_decompose_divprop [lemma, in sqrt_prog]

I_positive [lemma, in mpn_complements]

length_n_decompose [lemma, in memory]

le_ceildiv2' [lemma, in div2]

le_ceildiv2' [lemma, in fun_aux]

le_div2_minus [lemma, in sqrt_prog]

le_Zle [lemma, in nat_morphism2]

le_Zle [lemma, in nat_morphism]

lt1_le0 [lemma, in sqrt_prog]

lt_ceildiv2' [lemma, in fun_aux]

lt_ceildiv2' [lemma, in div2]

lt_floordiv [lemma, in fun_aux]

lt_floordiv [lemma, in div2]

lt_minus_div2 [lemma, in sqrt_prog]

lt_O_div2 [lemma, in sqrt_prog]

L1 [lemma, in proof_sqrt]

l1 [lemma, in lemmas]

l10 [lemma, in lemmas]

l11 [lemma, in lemmas]

l12 [lemma, in lemmas]

l14 [lemma, in lemmas]

l15 [lemma, in lemmas]

l16 [lemma, in lemmas]

l17 [lemma, in lemmas]

l2 [lemma, in lemmas]

L2 [lemma, in proof_sqrt]

L3 [lemma, in proof_sqrt]

l3 [lemma, in lemmas]

l4 [lemma, in lemmas]

L4 [lemma, in Zextensions]

L4' [lemma, in Zextensions]

L5 [lemma, in Zextensions]

l5 [lemma, in lemmas]

L6 [lemma, in Zextensions]

l6 [lemma, in lemmas]

l7 [lemma, in lemmas]

L7 [lemma, in Zextensions]

l8 [lemma, in lemmas]

l9 [lemma, in lemmas]

minus_div2_S [lemma, in sqrt_prog]

modZ [definition, in specifications]

modZtoZ [definition, in specifications]

modZ_xH [lemma, in specifications]

modZ_ZERO [lemma, in specifications]

mpn_complements [module]

mult_morphism [lemma, in nat_morphism]

mult_morphism [lemma, in nat_morphism2]

m1_m [lemma, in memory]

m2_m [lemma, in memory]

m2_m' [lemma, in memory]

nat_morphism [module]

nat_morphism2 [module]

nn_even_implies_2tn_is_nn [lemma, in top_sqrt]

nn_odd_implies_2tn_is_nn [lemma, in top_sqrt]

normalization_propagation [lemma, in proof_sqrt]

normalized_base_case [lemma, in fun]

normalized_base_case_aux [lemma, in fun]

normalized_divide [lemma, in fun_aux]

normalized_div2 [lemma, in fun_aux]

normalized_positive [lemma, in fun]

normalized_positive_l [lemma, in proof_sqrt]

no_overlap [definition, in specifications]

Npos [lemma, in proof_sqrt]

Ntstrictpos [lemma, in top_sqrt]

Ntsup [lemma, in top_sqrt]

Nts0 [lemma, in top_sqrt]

N''pos [lemma, in proof_sqrt]

N0ltL [lemma, in proof_sqrt]

N0pos [lemma, in proof_sqrt]

N1ltL [lemma, in proof_sqrt]

N1_22k_Nt [lemma, in top_sqrt]

one_le_minus_div2 [lemma, in sqrt_prog]

others_are_unchanged [lemma, in memory]

plus_morphism [lemma, in nat_morphism2]

Post_mpn_addmul_1 [definition, in specifications]

pow [definition, in pow]

pow [module]

powbetaGt0 [lemma, in top_sqrt]

pow_beta_b [lemma, in top_sqrt]

pow_b_is_even [lemma, in fun]

pow_ceil_ge_pow_floor [lemma, in div2]

pow_decompose [lemma, in div2]

pow_div2 [lemma, in sqrt_prog]

pow_h_ge_pow_l [lemma, in sqrt_prog]

pow_monotonous [lemma, in pow]

pow_morphism [lemma, in nat_morphism2]

pow_morphism [lemma, in nat_morphism]

pow_mult [lemma, in pow]

pow_nat [definition, in nat_morphism]

pow_nat [definition, in nat_morphism2]

pow_pos [lemma, in pow]

pow_positive [lemma, in mpn_complements]

pow_positive' [lemma, in sqrt_prog]

pow_sum [lemma, in pow]

proof_sqrt [module]

QleL [lemma, in proof_sqrt]

Qpos [lemma, in proof_sqrt]

quotype [inductive, in fun_aux]

quo_type_def [constructor, in fun_aux]

q0pos [lemma, in top_sqrt]

R''pos [lemma, in proof_sqrt]

R1 [definition, in proof_sqrt]

R2 [definition, in fun_aux]

R2_eq1 [lemma, in fun_aux]

R2_eq2 [lemma, in fun_aux]

shift_2 [definition, in specifications]

SolveBounds [tactic definition, in tacdef]

specifications [module]

sqrtrem [definition, in fun]

sqrtrembase [definition, in fun]

sqrtrembase [module]

sqrtrempos [definition, in sqrtrembase]

SqrtremProp [definition, in proof_sqrt]

SqrtremProp1 [definition, in proof_sqrt]

SqrtremProp2 [definition, in proof_sqrt]

SqrtremProp3 [definition, in proof_sqrt]

SqrtremProp4 [definition, in proof_sqrt]

sqrt_data [inductive, in sqrtrembase]

sqrt_F [definition, in fun]

sqrt_F_type [definition, in fun]

sqrt_goals [module]

sqrt_goals2 [module]

sqrt_goals3 [module]

sqrt_goals4 [module]

sqrt_goals9_1' [lemma, in build_aux_thms]

sqrt_goals9_2' [lemma, in build_aux_thms]

sqrt_goals9_3' [lemma, in build_aux_thms]

sqrt_goals9_4' [lemma, in build_aux_thms]

sqrt_goals9_5' [lemma, in build_aux_thms]

sqrt_goals9_6' [lemma, in build_aux_thms]

sqrt_goals9_7' [lemma, in build_aux_thms]

sqrt_goal1 [lemma, in sqrt_goals]

sqrt_goal10 [lemma, in sqrt_goals4]

sqrt_goal2 [lemma, in sqrt_goals]

sqrt_goal3 [lemma, in sqrt_goals]

sqrt_goal4 [lemma, in sqrt_goals]

sqrt_goal5 [lemma, in sqrt_goals]

sqrt_goal6 [lemma, in sqrt_goals2]

sqrt_goal7 [lemma, in sqrt_goals2]

sqrt_goal8 [lemma, in sqrt_goals2]

sqrt_goal9 [lemma, in sqrt_goals3]

sqrt_prog [module]

sqrt_prog1 [module]

square_monotone [lemma, in sqrt_prog]

square_positive [lemma, in sqrt_prog]

square_pow [lemma, in pow]

sub_goals [module]

sub_goals2 [module]

sub_goal1 [lemma, in sub_goals]

sub_goal2 [lemma, in sub_goals]

sub_goal3 [lemma, in sub_goals]

sub_goal4 [lemma, in sub_goals]

sub_goal5 [lemma, in sub_goals2]

sub_square [module]

suppress_1 [lemma, in lemmas]

s0pos [lemma, in top_sqrt]

S1 [definition, in proof_sqrt]

S1pos [lemma, in top_sqrt]

S2 [definition, in fun_aux]

S2pos [lemma, in proof_sqrt]

S2_eq1 [lemma, in fun_aux]

S2_eq2 [lemma, in fun_aux]

S3 [lemma, in proof_sqrt]

S4 [lemma, in proof_sqrt]

S_morphism [lemma, in nat_morphism2]

S_morphism [lemma, in nat_morphism]

thm_between [lemma, in top_sqrt]

thm_between' [lemma, in top_sqrt]

thm_between_Nt [lemma, in top_sqrt]

thm_final [lemma, in top_sqrt]

thm_Qdiv2q0 [lemma, in top_sqrt]

thm_q0s0 [lemma, in top_sqrt]

thm_R [lemma, in top_sqrt]

thm_R2 [lemma, in top_sqrt]

thm_R3 [lemma, in top_sqrt]

thm_R3' [lemma, in top_sqrt]

thm_R3'' [lemma, in top_sqrt]

thm_topsqrtremprop1 [lemma, in top_sqrt]

thm_Zsquare [lemma, in pow]

thm_Zsquare2 [lemma, in pow]

tn [definition, in top_sqrt]

top_misc [module]

top_sqrt [module]

two_step_ind [lemma, in sqrt_prog]

two_step_ind [lemma, in div2]

two_2 [lemma, in sqrt_prog]

T1 [lemma, in proof_sqrt]

T1_aux [lemma, in proof_sqrt]

Zdivprop1' [definition, in proof_sqrt]

Zdivprop2' [definition, in proof_sqrt]

Zdivprop3' [definition, in proof_sqrt]

Zdivprop4' [definition, in proof_sqrt]

Zextensions [module]

Zgt_not_le' [lemma, in Zextensions]

Zgt_S_le' [lemma, in Zextensions]

Zle_lt_1 [lemma, in Zextensions]

Zle_mult' [lemma, in Zextensions]

Zle_mult_simpl' [lemma, in Zextensions]

Zle_mult_2 [lemma, in mpn_complements]

Zle_Zmult_right' [lemma, in Zextensions]

Zle_Zmult_right2' [lemma, in Zextensions]

Zlt_left_plus [lemma, in Zextensions]

Zlt_mult_l [lemma, in sqrt_prog]

Zlt_mult_r [lemma, in sqrt_prog]

zlt_zero_beta [lemma, in sqrt_goals]

Zlt_Zmult_left [lemma, in Zextensions]

Zlt_Zmult_right [lemma, in Zextensions]

Zlt_Zmult_right2' [lemma, in Zextensions]

Zminus [definition, in correct_result]

Zminus_minus_assoc [lemma, in sqrt_prog]

Zminus_permute [lemma, in sqrt_prog]

Zminus_permute_square [lemma, in sqrt_prog]

Zminus_plus_assoc [lemma, in sqrt_prog]

Zminus_plus_permute [lemma, in sqrt_prog]

Zminus_plus_permute_square [lemma, in sqrt_prog]

Zminus_Zsquare [lemma, in pow]

Zmod [definition, in fun]

Zmultbool [definition, in specifications]

Zmultbool_to_Zmult [lemma, in sqrt_prog]

Zmult_le' [lemma, in Zextensions]

Zmult_lt' [lemma, in Zextensions]

Zmult_reg_left' [lemma, in Zextensions]

Zmult_reg_r [lemma, in lemmas]

Zmult_Zsquare [lemma, in pow]

Zplus_minus2 [lemma, in sqrt_prog]

Zplus_minus_assoc [lemma, in sqrt_prog]

Zplus_Zsquare [lemma, in pow]

Zquo [definition, in fun]

Zsquare [definition, in pow]

Zsquare_monotonous [lemma, in pow]

Zsquare_order [lemma, in pow]

Z0lt_le_pred [lemma, in Zextensions]

Z2bool [definition, in sqrt_prog]

Z_le_lt_dec [lemma, in Zextensions]

Z_lt_le_bool [definition, in correct_result]

Z_lt_le_dec [lemma, in Zextensions]

divDefBreakdown3 [in proof_sqrt]

divDefBreakdown4 [in proof_sqrt]

beta' [in specifications]

bound [in specifications]

add_un_add [in nat_morphism2]

add_un_add [in nat_morphism]

already_normalized_ok [in top_sqrt]

auxiliary_for_sqrt_goals1 [in sqrt_goals2]

aux_1 [in sqrt_prog]

aux_10 [in sqrt_prog]

aux_11 [in sqrt_prog]

aux_12 [in sqrt_prog]

aux_13 [in sqrt_prog]

aux_2 [in sqrt_prog]

aux_3 [in sqrt_prog]

aux_4 [in sqrt_prog]

aux_5 [in sqrt_prog]

aux_6 [in sqrt_prog]

aux_7 [in sqrt_prog]

aux_8 [in sqrt_prog]

aux_9 [in sqrt_prog]

A1 [in Zextensions]

A1' [in lemmas]

A2 [in Zextensions]

betaGt0 [in top_sqrt]

betaGt2 [in mpn_complements]

betaMultipleTwo [in top_sqrt]

between_0_1 [in sqrt_prog]

between_0_1' [in sqrt_prog]

borrow_bound [in mpn_complements]

borrow_positive [in mpn_complements]

borrow_positive' [in mpn_complements]

bPos [in fun]

bPowPos [in fun]

ceildiv2_aux_lemma [in div2]

ceildiv2_characteristic [in div2]

ceildiv2_eq [in div2]

correct_goal1 [in correct_goals]

correct_goal2 [in correct_goals]

correct_goal3 [in correct_goals]

correct_goal4 [in correct_goals]

correct_goal5 [in correct_goals]

correct_goal6 [in correct_goals]

correct_goal7 [in correct_goals]

div2_double_le [in sqrt_prog]

div2_floordiv2_equal [in sqrt_prog]

div2_le [in sqrt_prog]

div2_minus [in sqrt_prog]

div2_minus' [in sqrt_prog]

div2_minus_lt [in sqrt_prog]

div2_mult2 [in sqrt_prog]

div2_nn_l [in sqrt_prog]

div2_odd [in sqrt_prog]

div2_thm1 [in top_misc]

div2_thm2 [in top_misc]

div2_thm3 [in top_misc]

div2_thm4 [in top_misc]

div2_01 [in top_misc]

div_goal1 [in div_goals]

div_goal10 [in div_goals10]

div_goal11 [in div_goals11]

div_goal12 [in div_goals12]

div_goal13 [in div_goals13]

div_goal2 [in div_goals2]

div_goal3 [in div_goals3]

div_goal4 [in div_goals4]

div_goal5 [in div_goals5]

div_goal6 [in div_goals6]

div_goal7 [in div_goals7]

div_goal8 [in div_goals8]

div_goal9 [in div_goals9]

div_rem_uniqueness [in top_sqrt]

easy_thm2 [in top_sqrt]

exponentbMulipleFour [in fun_aux]

exponentbMulipleFour [in fun]

floordiv2_le_ceildiv2 [in div2]

former_prop4 [in proof_sqrt]

Hhalfpos [in proof_sqrt]

Hhalf_easy [in sqrt_prog]

Hpos [in proof_sqrt]

implies_normalized_N1 [in top_sqrt]

Impnumber_access [in mpn_complements]

Impnumber_between [in mpn_complements]

Impnumber_bound [in mpn_complements]

Impnumber_decompose [in mpn_complements]

Impnumber_unchanged [in mpn_complements]

Impnumber_unchanged_bis [in mpn_complements]

inj_minus_div2 [in sqrt_prog]

I_decompose_divprop [in sqrt_prog]

I_positive [in mpn_complements]

le_ceildiv2' [in div2]

le_ceildiv2' [in fun_aux]

le_div2_minus [in sqrt_prog]

le_Zle [in nat_morphism2]

le_Zle [in nat_morphism]

lt1_le0 [in sqrt_prog]

lt_ceildiv2' [in fun_aux]

lt_ceildiv2' [in div2]

lt_floordiv [in fun_aux]

lt_floordiv [in div2]

lt_minus_div2 [in sqrt_prog]

lt_O_div2 [in sqrt_prog]

L1 [in proof_sqrt]

l1 [in lemmas]

l10 [in lemmas]

l11 [in lemmas]

l12 [in lemmas]

l14 [in lemmas]

l15 [in lemmas]

l16 [in lemmas]

l17 [in lemmas]

l2 [in lemmas]

L2 [in proof_sqrt]

L3 [in proof_sqrt]

l3 [in lemmas]

l4 [in lemmas]

L4 [in Zextensions]

L4' [in Zextensions]

L5 [in Zextensions]

l5 [in lemmas]

L6 [in Zextensions]

l6 [in lemmas]

l7 [in lemmas]

L7 [in Zextensions]

l8 [in lemmas]

l9 [in lemmas]

modZ_xH [in specifications]

modZ_ZERO [in specifications]

mult_morphism [in nat_morphism]

mult_morphism [in nat_morphism2]

m1_m [in memory]

m2_m [in memory]

m2_m' [in memory]

nn_odd_implies_2tn_is_nn [in top_sqrt]

normalization_propagation [in proof_sqrt]

normalized_base_case [in fun]

normalized_base_case_aux [in fun]

normalized_divide [in fun_aux]

normalized_div2 [in fun_aux]

normalized_positive [in fun]

normalized_positive_l [in proof_sqrt]

Npos [in proof_sqrt]

Ntstrictpos [in top_sqrt]

Ntsup [in top_sqrt]

Nts0 [in top_sqrt]

N''pos [in proof_sqrt]

N0ltL [in proof_sqrt]

N0pos [in proof_sqrt]

N1ltL [in proof_sqrt]

N1_22k_Nt [in top_sqrt]

others_are_unchanged [in memory]

plus_morphism [in nat_morphism2]

powbetaGt0 [in top_sqrt]

pow_beta_b [in top_sqrt]

pow_b_is_even [in fun]

pow_ceil_ge_pow_floor [in div2]

pow_decompose [in div2]

pow_div2 [in sqrt_prog]

pow_h_ge_pow_l [in sqrt_prog]

pow_monotonous [in pow]

pow_morphism [in nat_morphism2]

pow_morphism [in nat_morphism]

pow_mult [in pow]

pow_pos [in pow]

pow_positive [in mpn_complements]

pow_positive' [in sqrt_prog]

pow_sum [in pow]

QleL [in proof_sqrt]

Qpos [in proof_sqrt]

q0pos [in top_sqrt]

R''pos [in proof_sqrt]

R2_eq1 [in fun_aux]

R2_eq2 [in fun_aux]

sqrt_goals9_1' [in build_aux_thms]

sqrt_goals9_2' [in build_aux_thms]

sqrt_goals9_3' [in build_aux_thms]

sqrt_goals9_4' [in build_aux_thms]

sqrt_goals9_5' [in build_aux_thms]

sqrt_goals9_6' [in build_aux_thms]

sqrt_goals9_7' [in build_aux_thms]

sqrt_goal1 [in sqrt_goals]

sqrt_goal10 [in sqrt_goals4]

sqrt_goal2 [in sqrt_goals]

sqrt_goal3 [in sqrt_goals]

sqrt_goal4 [in sqrt_goals]

sqrt_goal5 [in sqrt_goals]

sqrt_goal6 [in sqrt_goals2]

sqrt_goal7 [in sqrt_goals2]

sqrt_goal8 [in sqrt_goals2]

sqrt_goal9 [in sqrt_goals3]

square_monotone [in sqrt_prog]

square_positive [in sqrt_prog]

square_pow [in pow]

sub_goal1 [in sub_goals]

sub_goal2 [in sub_goals]

sub_goal3 [in sub_goals]

sub_goal4 [in sub_goals]

sub_goal5 [in sub_goals2]

suppress_1 [in lemmas]

s0pos [in top_sqrt]

S1pos [in top_sqrt]

S2pos [in proof_sqrt]

S2_eq1 [in fun_aux]

S2_eq2 [in fun_aux]

S3 [in proof_sqrt]

S4 [in proof_sqrt]

S_morphism [in nat_morphism2]

S_morphism [in nat_morphism]

thm_between' [in top_sqrt]

thm_between_Nt [in top_sqrt]

thm_final [in top_sqrt]

thm_Qdiv2q0 [in top_sqrt]

thm_q0s0 [in top_sqrt]

thm_R [in top_sqrt]

thm_R2 [in top_sqrt]

thm_R3 [in top_sqrt]

thm_R3' [in top_sqrt]

thm_R3'' [in top_sqrt]

thm_topsqrtremprop1 [in top_sqrt]

thm_Zsquare [in pow]

thm_Zsquare2 [in pow]

two_step_ind [in sqrt_prog]

two_step_ind [in div2]

two_2 [in sqrt_prog]

T1 [in proof_sqrt]

T1_aux [in proof_sqrt]

Zgt_S_le' [in Zextensions]

Zle_lt_1 [in Zextensions]

Zle_mult' [in Zextensions]

Zle_mult_simpl' [in Zextensions]

Zle_mult_2 [in mpn_complements]

Zle_Zmult_right' [in Zextensions]

Zle_Zmult_right2' [in Zextensions]

Zlt_left_plus [in Zextensions]

Zlt_mult_l [in sqrt_prog]

Zlt_mult_r [in sqrt_prog]

zlt_zero_beta [in sqrt_goals]

Zlt_Zmult_left [in Zextensions]

Zlt_Zmult_right [in Zextensions]

Zlt_Zmult_right2' [in Zextensions]

Zminus_minus_assoc [in sqrt_prog]

Zminus_permute [in sqrt_prog]

Zminus_permute_square [in sqrt_prog]

Zminus_plus_assoc [in sqrt_prog]

Zminus_plus_permute [in sqrt_prog]

Zminus_plus_permute_square [in sqrt_prog]

Zminus_Zsquare [in pow]

Zmultbool_to_Zmult [in sqrt_prog]

Zmult_le' [in Zextensions]

Zmult_lt' [in Zextensions]

Zmult_reg_left' [in Zextensions]

Zmult_reg_r [in lemmas]

Zmult_Zsquare [in pow]

Zplus_minus2 [in sqrt_prog]

Zplus_minus_assoc [in sqrt_prog]

Zplus_Zsquare [in pow]

Zsquare_monotonous [in pow]

Zsquare_order [in pow]

Z0lt_le_pred [in Zextensions]

Z_le_lt_dec [in Zextensions]

Z_lt_le_dec [in Zextensions]

c_sqrt [in sqrtrembase]

b [in top_sqrt]

beta [in top_sqrt]

beta [in specifications]

bool2nat [in sqrt_prog]

bool2Z [in sqrt_prog]

ceildiv2 [in div2]

ceildiv2' [in div2]

divrem' [in fun]

div2' [in sqrt_prog]

f' [in specifications]

isEvenOrOdd [in specifications]

IsNormalized [in proof_sqrt]

modZtoZ [in specifications]

pow [in pow]

pow_nat [in nat_morphism]

pow_nat [in nat_morphism2]

R2 [in fun_aux]

sqrtrem [in fun]

sqrtrembase [in fun]

sqrtrempos [in sqrtrembase]

SqrtremProp [in proof_sqrt]

SqrtremProp1 [in proof_sqrt]

SqrtremProp2 [in proof_sqrt]

SqrtremProp3 [in proof_sqrt]

SqrtremProp4 [in proof_sqrt]

sqrt_F [in fun]

sqrt_F_type [in fun]

S1 [in proof_sqrt]

S2 [in fun_aux]

Zdivprop1' [in proof_sqrt]

Zdivprop2' [in proof_sqrt]

Zdivprop3' [in proof_sqrt]

Zdivprop4' [in proof_sqrt]

Zminus [in correct_result]

Zmod [in fun]

Zmultbool [in specifications]

Zquo [in fun]

Zsquare [in pow]

Z2bool [in sqrt_prog]

Z_lt_le_bool [in correct_result]

correct_goals

correct_result

div2

div_goals

div_goals10

div_goals11

div_goals12

div_goals13

div_goals2

div_goals3

div_goals4

div_goals5

div_goals6

div_goals7

div_goals8

div_goals9

fun_aux

mpn_complements

nat_morphism2

proof_sqrt

sqrtrembase

sqrt_goals

sqrt_goals2

sqrt_goals3

sqrt_goals4

sqrt_prog

sqrt_prog1

sub_goals

sub_goals2

sub_square

top_misc

top_sqrt

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (390 entries) |

Tactic Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (6 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (277 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (54 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (44 entries) |

This page has been generated by coqdoc