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 _ other (18818 entries)
Instance 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 _ other (548 entries)
Projection 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 _ other (206 entries)
Record 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 _ other (68 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 _ other (8939 entries)
Section 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 _ other (338 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 _ other (422 entries)
Notation 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 _ other (644 entries)
Abbreviation 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 _ other (1243 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 _ other (209 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 _ other (2935 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 _ other (703 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 _ other (699 entries)
Variable 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 _ other (1456 entries)
Library 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 _ other (408 entries)

Z (variable)

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


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 _ other (18818 entries)
Instance 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 _ other (548 entries)
Projection 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 _ other (206 entries)
Record 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 _ other (68 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 _ other (8939 entries)
Section 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 _ other (338 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 _ other (422 entries)
Notation 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 _ other (644 entries)
Abbreviation 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 _ other (1243 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 _ other (209 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 _ other (2935 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 _ other (703 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 _ other (699 entries)
Variable 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 _ other (1456 entries)
Library 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 _ other (408 entries)