Z (variable)
ZAddOrderProp.PosNeg.P [in P]
ZAddOrderProp.PosNeg.P_wd [in P_wd]
Zip.A [in A]
Zip.B [in B]
Zip.C [in C]
Zip.f [in f]
Zlength_properties.A [in A]
ZModulo.digits [in digits]
ZModulo.digits_gt_1 [in digits_gt_1]
ZModulo.digits_ne_1 [in digits_ne_1]
ZnZ.Specs.wB [in wB]
ZnZ.WW.wB [in wB]
Zn2Z.znz [in znz]
ZPairsAxiomsMod.Induction.A [in A]
ZPairsAxiomsMod.Induction.A_wd [in A_wd]
ZTypeIsZAxioms.Induction.A [in A]
ZTypeIsZAxioms.Induction.AS [in AS]
ZTypeIsZAxioms.Induction.A_wd [in A_wd]
ZTypeIsZAxioms.Induction.A0 [in A0]
ZTypeIsZAxioms.Induction.B [in B]
Z_2nZ.w_opp [in w_opp]
Z_2nZ.w_mod_gt [in w_mod_gt]
Z_2nZ.spec_ww_sqrt2 [in spec_ww_sqrt2]
Z_2nZ.mul [in mul]
Z_2nZ.gcd [in gcd]
Z_2nZ.spec_ww_opp [in spec_ww_opp]
Z_2nZ.sub [in sub]
Z_2nZ.spec_ww_head0 [in spec_ww_head0]
Z_2nZ.spec_ww_digits [in spec_ww_digits]
Z_2nZ.sub_carry_c [in sub_carry_c]
Z_2nZ.succ [in succ]
Z_2nZ.wB [in wB]
Z_2nZ.spec_low [in spec_low]
Z_2nZ.w_is_even [in w_is_even]
Z_2nZ.gcd_gt [in gcd_gt]
Z_2nZ.w_sub_carry_c [in w_sub_carry_c]
Z_2nZ.spec_ww_gcd [in spec_ww_gcd]
Z_2nZ.w_of_pos [in w_of_pos]
Z_2nZ.w_div21 [in w_div21]
Z_2nZ.add [in add]
Z_2nZ.w_gcd [in w_gcd]
Z_2nZ.square_c [in square_c]
Z_2nZ.gcd_gt_fix [in gcd_gt_fix]
Z_2nZ.spec_add2 [in spec_add2]
Z_2nZ.w_gcd_gt [in w_gcd_gt]
Z_2nZ.spec_ww_eq0 [in spec_ww_eq0]
Z_2nZ.w_add2 [in w_add2]
Z_2nZ.spec_ww_sub [in spec_ww_sub]
Z_2nZ.w_eq0 [in w_eq0]
Z_2nZ.w_digits [in w_digits]
Z_2nZ.spec_ww_add_c [in spec_ww_add_c]
Z_2nZ.spec_ww_1 [in spec_ww_1]
Z_2nZ.w_pos_mod [in w_pos_mod]
Z_2nZ.gcd_cont [in gcd_cont]
Z_2nZ.w_mul_c [in w_mul_c]
Z_2nZ.spec_ww_mul_c [in spec_ww_mul_c]
Z_2nZ.tail0 [in tail0]
Z_2nZ._ww_digits [in _ww_digits]
Z_2nZ.eq0 [in eq0]
Z_2nZ.is_even [in is_even]
Z_2nZ.spec_ww_Bm1 [in spec_ww_Bm1]
Z_2nZ.w_add_carry_c [in w_add_carry_c]
Z_2nZ.sub_c [in sub_c]
Z_2nZ.div_gt [in div_gt]
Z_2nZ.mod_gt [in mod_gt]
Z_2nZ.w_head0 [in w_head0]
Z_2nZ._zn2z [in _zn2z]
Z_2nZ.spec_ww_pred [in spec_ww_pred]
Z_2nZ.opp_carry [in opp_carry]
Z_2nZ.sub_carry [in sub_carry]
Z_2nZ.to_Z [in to_Z]
Z_2nZ.wwB [in wwB]
Z_2nZ.add_c [in add_c]
Z_2nZ.spec_ww_square_c [in spec_ww_square_c]
Z_2nZ.w_sub [in w_sub]
Z_2nZ.spec_ww_sub_carry [in spec_ww_sub_carry]
Z_2nZ.w_compare [in w_compare]
Z_2nZ.compare [in compare]
Z_2nZ.w_succ [in w_succ]
Z_2nZ.spec_ww_opp_c [in spec_ww_opp_c]
Z_2nZ.spec_ww_0 [in spec_ww_0]
Z_2nZ.head0 [in head0]
Z_2nZ.spec_ww_is_even [in spec_ww_is_even]
Z_2nZ.w_sub_c [in w_sub_c]
Z_2nZ.w_opp_c [in w_opp_c]
Z_2nZ.pred_c [in pred_c]
Z_2nZ.spec_ww_sqrt [in spec_ww_sqrt]
Z_2nZ.mod_ [in mod_]
Z_2nZ.karatsuba_c [in karatsuba_c]
Z_2nZ.w_div [in w_div]
Z_2nZ.sqrt2 [in sqrt2]
Z_2nZ.add_carry_c [in add_carry_c]
Z_2nZ.spec_ww_div [in spec_ww_div]
Z_2nZ.w_add_c [in w_add_c]
Z_2nZ.spec_ww_tail00 [in spec_ww_tail00]
Z_2nZ.spec_ww_of_pos [in spec_ww_of_pos]
Z_2nZ.mul_c [in mul_c]
Z_2nZ.w_add [in w_add]
Z_2nZ.w_1 [in w_1]
Z_2nZ.ww_of_pos [in ww_of_pos]
Z_2nZ.w_div_gt [in w_div_gt]
Z_2nZ.w_mul [in w_mul]
Z_2nZ.spec_ww_div_gt [in spec_ww_div_gt]
Z_2nZ.w_succ_c [in w_succ_c]
Z_2nZ.spec_ww_add [in spec_ww_add]
Z_2nZ.spec_ww_sub_carry_c [in spec_ww_sub_carry_c]
Z_2nZ.w_to_Z [in w_to_Z]
Z_2nZ.pred [in pred]
Z_2nZ.w_Bm1 [in w_Bm1]
Z_2nZ.spec_ww_compare [in spec_ww_compare]
Z_2nZ.ww_0W [in ww_0W]
Z_2nZ.w_sub_carry [in w_sub_carry]
Z_2nZ.spec_ww_gcd_gt [in spec_ww_gcd_gt]
Z_2nZ.spec_ww_sub_c [in spec_ww_sub_c]
Z_2nZ.spec_ww_add_carry [in spec_ww_add_carry]
Z_2nZ.add_carry [in add_carry]
Z_2nZ.w_add_carry [in w_add_carry]
Z_2nZ.sqrt [in sqrt]
Z_2nZ.ww_W0 [in ww_W0]
Z_2nZ.opp [in opp]
Z_2nZ.ww_Bm1 [in ww_Bm1]
Z_2nZ.spec_ww_mul [in spec_ww_mul]
Z_2nZ.w_opp_carry [in w_opp_carry]
Z_2nZ.div [in div]
Z_2nZ.w_WW [in w_WW]
Z_2nZ.spec_ww_karatsuba_c [in spec_ww_karatsuba_c]
Z_2nZ.add_mul_div [in add_mul_div]
Z_2nZ.spec_ww_mod [in spec_ww_mod]
Z_2nZ.w_add_mul_div [in w_add_mul_div]
Z_2nZ.w_pred_c [in w_pred_c]
Z_2nZ.w_pred [in w_pred]
Z_2nZ.div32 [in div32]
Z_2nZ._ww_zdigits [in _ww_zdigits]
Z_2nZ.spec_ww_head00 [in spec_ww_head00]
Z_2nZ.w_0 [in w_0]
Z_2nZ.ww_1 [in ww_1]
Z_2nZ.w_sqrt2 [in w_sqrt2]
Z_2nZ.w_W0 [in w_W0]
Z_2nZ.w_sqrt [in w_sqrt]
Z_2nZ.pos_mod [in pos_mod]
Z_2nZ.ww_WW [in ww_WW]
Z_2nZ.spec_ww_tail0 [in spec_ww_tail0]
Z_2nZ.w_square_c [in w_square_c]
Z_2nZ.opp_c [in opp_c]
Z_2nZ.spec_ww_pred_c [in spec_ww_pred_c]
Z_2nZ.succ_c [in succ_c]
Z_2nZ.low [in low]
Z_2nZ.w_mod [in w_mod]
Z_2nZ.spec_ww_div21 [in spec_ww_div21]
Z_2nZ.spec_ww_opp_carry [in spec_ww_opp_carry]
Z_2nZ.div21 [in div21]
Z_2nZ.spec_ww_add_carry_c [in spec_ww_add_carry_c]
Z_2nZ.w_Bm2 [in w_Bm2]
Z_2nZ.spec_ww_succ [in spec_ww_succ]
Z_2nZ.spec_ww_mod_gt [in spec_ww_mod_gt]
Z_2nZ.w_0W [in w_0W]
Z_2nZ.spec_w_div32 [in spec_w_div32]
Z_2nZ.w_zdigits [in w_zdigits]
Z_2nZ.spec_ww_to_Z [in spec_ww_to_Z]
Z_2nZ.w_tail0 [in w_tail0]
Z_2nZ.spec_ww_succ_c [in spec_ww_succ_c]