Global Index

G

J

K

V

W

Y

_

(1380 entries)

Notation Index

A

B

C

D

E

F

G

H

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(31 entries)

Variable Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Library Index

B

C

D

F

G

J

K

O

T

U

V

W

X

Y

_

other

(25 entries)

Lemma Index

B

F

G

H

I

J

K

N

Q

U

V

W

X

Y

_

other

(697 entries)

Axiom Index

A

B

D

G

H

J

K

N

Q

T

U

V

W

Y

Z

_

other

(223 entries)

Constructor Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Inductive Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Section Index

C

D

F

G

H

J

K

O

Q

S

T

U

V

W

X

Y

Z

_

other

(119 entries)

Definition Index

A

D

G

H

I

J

K

N

O

T

V

W

X

Y

_

other

(271 entries)

Global Index

A

ABSZ [lemma, in Rational.Integer.Absz]
AbsZ [section, in Rational.Integer.Absz]
ABSZ [lemma, in Rational.Integer.Absz]
AbsZ [section, in Rational.Integer.Absz]
ABSZ [lemma, in Rational.Integer.Absz]
ABSZ [lemma, in Rational.Integer.Absz]
AbsZ [section, in Rational.Integer.Absz]
AbsZ [section, in Rational.Integer.Absz]
Absz [library]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
ABSZ_O [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_O [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
ABSZ_O [lemma, in Rational.Integer.Absz]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_O [lemma, in Rational.Integer.Absz]
ABSZ_O [lemma, in Rational.Integer.Absz]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_O [lemma, in Rational.Integer.Absz]
ABSZ_neg [lemma, in Rational.Integer.Absz]
ABSZ_pos [lemma, in Rational.Integer.Absz]
AC [library]

B

binary_minusQ [definition, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]
binary_minus [section, in Rational.Rational.minus]
binary_minusQ [definition, in Rational.Rational.minus]

C

Canonic [axiom, in Rational.Subset.subset]
Canonic [axiom, in Rational.Subset.subset]
Canonic [axiom, in Rational.Subset.subset]
Canonic [axiom, in Rational.Subset.subset]
Canonic [axiom, in Rational.Subset.subset]
Canonic [axiom, in Rational.Subset.subset]
Canonic [axiom, in Rational.Subset.subset]
Closure [axiom, in Rational.Quotient.quotient]
Closure [axiom, in Rational.Quotient.quotient]
Closure [axiom, in Rational.Quotient.quotient]
Closure [axiom, in Rational.Quotient.quotient]
Closure [axiom, in Rational.Quotient.quotient]
Closure [axiom, in Rational.Quotient.quotient]
Closure [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Closure_prop [axiom, in Rational.Quotient.quotient]
Compat [definition, in Rational.Quotient.quotient]
Compat [definition, in Rational.Quotient.quotient]
Compat [definition, in Rational.Quotient.quotient]
Compat [definition, in Rational.Quotient.quotient]
Compat [definition, in Rational.Quotient.quotient]
Compat [definition, in Rational.Quotient.quotient]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_prop [definition, in Rational.Quotient.quotient]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_PX [lemma, in Rational.Quotient.extensionality]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_leZ_X [lemma, in Rational.Integer.leZ]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_multZ_X [lemma, in Rational.Integer.integer_defs]
Compat_multQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_plusZ_XX [lemma, in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [lemma, in Rational.Rational.minus]
Compat_swap [lemma, in Rational.Integer.integer_defs]
Compat_multQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_X [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusQ_XX [lemma, in Rational.Rational.rational_defs]
Compat_plusZ_X [lemma, in Rational.Integer.integer_defs]
Compat_leZ_XX [lemma, in Rational.Integer.leZ]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]
Constructive_Z_partition [lemma, in Rational.Integer.leZproperties]

D

distribQ [lemma, in Rational.Rational.MultQ]
distribQ [lemma, in Rational.Rational.MultQ]
distribQ [lemma, in Rational.Rational.MultQ]
distribQ [lemma, in Rational.Rational.MultQ]
distribQ [lemma, in Rational.Rational.MultQ]
distribQ [lemma, in Rational.Rational.MultQ]
distribQ [lemma, in Rational.Rational.MultQ]
distribQ [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribQ_l [lemma, in Rational.Rational.MultQ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]
distribZ_l [lemma, in Rational.Integer.MultZ]

E

E [definition, in Rational.Quotient.extensionality]
eq_ext [definition, in Rational.Quotient.extensionality]
eq_ext [definition, in Rational.Quotient.extensionality]
eq_pair [lemma, in Rational.Integer.integer_defs]
eq_pair [lemma, in Rational.Integer.integer_defs]
eq_pair [lemma, in Rational.Integer.integer_defs]
eq_ext [definition, in Rational.Quotient.extensionality]
eq_pair [lemma, in Rational.Integer.integer_defs]
eq_pair [lemma, in Rational.Integer.integer_defs]
eq_ext [definition, in Rational.Quotient.extensionality]
eq_pair [lemma, in Rational.Integer.integer_defs]
eq_pair [lemma, in Rational.Integer.integer_defs]
eq_ext [definition, in Rational.Quotient.extensionality]
eq_ext [definition, in Rational.Quotient.extensionality]
EXP [inductive, in Rational.Integer.leZproperties]
EXP [inductive, in Rational.Integer.leZproperties]
EXP [inductive, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
EXP_intro [constructor, in Rational.Integer.leZproperties]
Ext [axiom, in Rational.Quotient.quotient]
Ext [axiom, in Rational.Quotient.quotient]
Ext [axiom, in Rational.Quotient.quotient]
extensionality [lemma, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
extensionality [lemma, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
Extensionality [section, in Rational.Quotient.extensionality]
extensionality [library]
Extensionality.A [variable, in Rational.Quotient.extensionality]
Extensionality.B [variable, in Rational.Quotient.extensionality]

F

fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
fromZ_to_Q [definition, in Rational.Rational.Z_to_Q]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_R_to_L [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]
From_L_to_R [axiom, in Rational.Quotient.quotient]

H

HeadSimpl [library]
HS [library]

I

In [axiom, in Rational.Quotient.quotient]
In [axiom, in Rational.Quotient.quotient]
INT [section, in Rational.Integer.int]
INT [section, in Rational.Integer.int]
INT [section, in Rational.Integer.int]
int [library]
integer [library]
Integers [section, in Rational.Integer.integer_defs]
Integers [section, in Rational.Integer.integer_defs]
Integers [section, in Rational.Integer.integer_defs]
Integers [section, in Rational.Integer.integer_defs]
Integers [section, in Rational.Integer.integer_defs]
Integers [section, in Rational.Integer.integer_defs]
Integers [section, in Rational.Integer.integer_defs]
Integers [section, in Rational.Integer.integer_defs]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
Integers_are_Rationals [section, in Rational.Rational.Z_to_Q]
_ + _ (INT_scope) [notation, in Rational.Integer.integer_defs]
integer_defs [library]
intnumbers [library]
In_subset [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_Out [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_Out [axiom, in Rational.Subset.subset]
In_Out [axiom, in Rational.Subset.subset]
In_Out [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_Out [axiom, in Rational.Subset.subset]
In_subset [axiom, in Rational.Subset.subset]
In_Out [axiom, in Rational.Subset.subset]

L

leZ [definition, in Rational.Integer.leZ]
LEZ [section, in Rational.Integer.leZ]
LEZ [section, in Rational.Integer.leZ]
LEZ [section, in Rational.Integer.leZ]
leZ [definition, in Rational.Integer.leZ]
leZ [definition, in Rational.Integer.leZ]
leZ [library]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [section, in Rational.Integer.leZproperties]
leZproperties [library]
leZ_XX [definition, in Rational.Integer.leZ]
leZ_XX [definition, in Rational.Integer.leZ]
leZ_XX [definition, in Rational.Integer.leZ]
leZ_XX [definition, in Rational.Integer.leZ]
leZ_XX [definition, in Rational.Integer.leZ]
leZ_X [definition, in Rational.Integer.leZ]
leZ_X [definition, in Rational.Integer.leZ]
leZ_XX [definition, in Rational.Integer.leZ]
leZ_X [definition, in Rational.Integer.leZ]
leZ_X [definition, in Rational.Integer.leZ]
leZ_X [definition, in Rational.Integer.leZ]
_ <= _ (INT_scope) [notation, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_false [lemma, in Rational.Integer.leZproperties]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_false [lemma, in Rational.Integer.leZproperties]
le_false [lemma, in Rational.Integer.leZproperties]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_false [lemma, in Rational.Integer.leZproperties]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_false [lemma, in Rational.Integer.leZproperties]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_with_plus2 [lemma, in Rational.Integer.leZ]
le_false [lemma, in Rational.Integer.leZproperties]
le_with_plus1 [lemma, in Rational.Integer.leZ]
le_false [lemma, in Rational.Integer.leZproperties]
le_false [lemma, in Rational.Integer.leZproperties]
lift [axiom, in Rational.Quotient.quotient]
lift [axiom, in Rational.Quotient.quotient]
lift [axiom, in Rational.Quotient.quotient]
lift [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
lift_prop [axiom, in Rational.Quotient.quotient]
ltZ [definition, in Rational.Integer.leZ]
ltZ [definition, in Rational.Integer.leZ]
ltZ [definition, in Rational.Integer.leZ]

M

minus [section, in Rational.Rational.minus]
minus [section, in Rational.Rational.minus]
minus [section, in Rational.Rational.minus]
minus [section, in Rational.Rational.minus]
minus [section, in Rational.Rational.minus]
minus [library]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_QUO [axiom, in Rational.Quotient.quotient]
MK_QUO [axiom, in Rational.Quotient.quotient]
MK_QUO [axiom, in Rational.Quotient.quotient]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_QUO [axiom, in Rational.Quotient.quotient]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_QUO [axiom, in Rational.Quotient.quotient]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_SUBSET [axiom, in Rational.Subset.subset]
MK_QUO [axiom, in Rational.Quotient.quotient]
MK_SUBSET [axiom, in Rational.Subset.subset]
multQ [definition, in Rational.Rational.rational_defs]
multQ [definition, in Rational.Rational.rational_defs]
MultQ [section, in Rational.Rational.MultQ]
MultQ [section, in Rational.Rational.MultQ]
multQ [definition, in Rational.Rational.rational_defs]
MultQ [section, in Rational.Rational.MultQ]
multQ [definition, in Rational.Rational.rational_defs]
MultQ [section, in Rational.Rational.MultQ]
MultQ [section, in Rational.Rational.MultQ]
multQ [definition, in Rational.Rational.rational_defs]
MultQ [library]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_X [definition, in Rational.Rational.rational_defs]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_X [definition, in Rational.Rational.rational_defs]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_X [definition, in Rational.Rational.rational_defs]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_X [definition, in Rational.Rational.rational_defs]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_X [definition, in Rational.Rational.rational_defs]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_X [definition, in Rational.Rational.rational_defs]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_XXX [definition, in Rational.Rational.rational_defs]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_X [definition, in Rational.Rational.rational_defs]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_XX [definition, in Rational.Rational.rational_defs]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_simpl_l [lemma, in Rational.Rational.rat]
multQ_sym [lemma, in Rational.Rational.MultQ]
multQ_assoc_l [lemma, in Rational.Rational.MultQ]
multQ_permute [lemma, in Rational.Rational.MultQ]
multQ_assoc_r [lemma, in Rational.Rational.MultQ]
multQ_permute [lemma, in Rational.Rational.MultQ]
MultZ [section, in Rational.Integer.MultZ]
multZ [definition, in Rational.Integer.integer_defs]
MultZ [section, in Rational.Integer.MultZ]
MultZ [section, in Rational.Integer.MultZ]
multZ [definition, in Rational.Integer.integer_defs]
MultZ [section, in Rational.Integer.MultZ]
multZ [definition, in Rational.Integer.integer_defs]
multZ [definition, in Rational.Integer.integer_defs]
MultZ [section, in Rational.Integer.MultZ]
multZ [definition, in Rational.Integer.integer_defs]
MultZ [library]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_X [definition, in Rational.Integer.integer_defs]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_XX [definition, in Rational.Integer.integer_defs]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_O [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_O [lemma, in Rational.Integer.MultZ]
multZ_O [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_XX [definition, in Rational.Integer.integer_defs]
multZ_X [definition, in Rational.Integer.integer_defs]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_O [lemma, in Rational.Integer.MultZ]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_XX [definition, in Rational.Integer.integer_defs]
multZ_XX [definition, in Rational.Integer.integer_defs]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_XX [definition, in Rational.Integer.integer_defs]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_X [definition, in Rational.Integer.integer_defs]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_X [definition, in Rational.Integer.integer_defs]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_O [lemma, in Rational.Integer.MultZ]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_XX [definition, in Rational.Integer.integer_defs]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_XXX [definition, in Rational.Integer.integer_defs]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_sym [lemma, in Rational.Integer.MultZ]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_O [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_O [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_X [definition, in Rational.Integer.integer_defs]
multZ_permute [lemma, in Rational.Integer.MultZ]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_X [definition, in Rational.Integer.integer_defs]
multZ_X [definition, in Rational.Integer.integer_defs]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_assoc_r [lemma, in Rational.Integer.MultZ]
multZ_simpl_l [axiom, in Rational.Integer.int]
multZ_assoc_l [lemma, in Rational.Integer.MultZ]
multZ_XX [definition, in Rational.Integer.integer_defs]
multZ_XX [definition, in Rational.Integer.integer_defs]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_permute [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_plus_distr_l [lemma, in Rational.Natural.NATURAL]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]
mult_minus [axiom, in Rational.Integer.MultZ]
mult_simpl_l [lemma, in Rational.Natural.NATURAL]

N

NAT [section, in Rational.Natural.NATURAL]
NAT [section, in Rational.Natural.NATURAL]
NAT [section, in Rational.Natural.NATURAL]
nat [library]
NATURAL [library]

O

one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
one_is_a_denominator [lemma, in Rational.Rational.Z_to_Q]
Out_subset [axiom, in Rational.Subset.subset]
Out_In [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_In [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_In [axiom, in Rational.Subset.subset]
Out_In [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_In [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
Out_In [axiom, in Rational.Subset.subset]
Out_subset [axiom, in Rational.Subset.subset]
O_lt_z [lemma, in Rational.Integer.leZproperties]
O_lt_z [lemma, in Rational.Integer.leZproperties]
O_lt_z [lemma, in Rational.Integer.leZproperties]
O_lt_z [lemma, in Rational.Integer.leZproperties]
O_lt_z [lemma, in Rational.Integer.leZproperties]
O_lt_z [lemma, in Rational.Integer.leZproperties]

P

P [definition, in Rational.Quotient.extensionality]
plusQ [section, in Rational.Rational.PlusQ]
plusQ [definition, in Rational.Rational.rational_defs]
plusQ [section, in Rational.Rational.PlusQ]
plusQ [section, in Rational.Rational.PlusQ]
plusQ [section, in Rational.Rational.PlusQ]
plusQ [definition, in Rational.Rational.rational_defs]
plusQ [section, in Rational.Rational.PlusQ]
plusQ [definition, in Rational.Rational.rational_defs]
plusQ [definition, in Rational.Rational.rational_defs]
plusQ [definition, in Rational.Rational.rational_defs]
PlusQ [library]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_X [definition, in Rational.Rational.rational_defs]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_X [definition, in Rational.Rational.rational_defs]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_X [definition, in Rational.Rational.rational_defs]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_sym [lemma, in Rational.Rational.PlusQ]
plusQ_X [definition, in Rational.Rational.rational_defs]
plusQ_XX [definition, in Rational.Rational.rational_defs]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_X [definition, in Rational.Rational.rational_defs]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_X [definition, in Rational.Rational.rational_defs]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_XXX [definition, in Rational.Rational.rational_defs]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_X [definition, in Rational.Rational.rational_defs]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_l [lemma, in Rational.Rational.PlusQ]
plusQ_plus_l [axiom, in Rational.Rational.PlusQ]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_permute [lemma, in Rational.Rational.PlusQ]
plusQ_assoc_r [lemma, in Rational.Rational.PlusQ]
plusQ_simpl_l [lemma, in Rational.Rational.rat]
plusQ_XXX_prelim [axiom, in Rational.Rational.rational_defs]
plusZ [definition, in Rational.Integer.integer_defs]
plusZ [definition, in Rational.Integer.integer_defs]
PlusZ [section, in Rational.Integer.PlusZ]
PlusZ [section, in Rational.Integer.PlusZ]
PlusZ [section, in Rational.Integer.PlusZ]
PlusZ [section, in Rational.Integer.PlusZ]
PlusZ [section, in Rational.Integer.PlusZ]
plusZ [definition, in Rational.Integer.integer_defs]
plusZ [definition, in Rational.Integer.integer_defs]
plusZ [definition, in Rational.Integer.integer_defs]
PlusZ [library]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_X [definition, in Rational.Integer.integer_defs]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_O [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_O [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_O [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_X [definition, in Rational.Integer.integer_defs]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_X [definition, in Rational.Integer.integer_defs]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_O [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_X [definition, in Rational.Integer.integer_defs]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_O [lemma, in Rational.Integer.PlusZ]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_X [definition, in Rational.Integer.integer_defs]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_XX [definition, in Rational.Integer.integer_defs]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_O [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_O [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_X [definition, in Rational.Integer.integer_defs]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_plus_l [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_X [definition, in Rational.Integer.integer_defs]
plusZ_sym [lemma, in Rational.Integer.PlusZ]
plusZ_permute [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_r [lemma, in Rational.Integer.PlusZ]
plusZ_XXX [definition, in Rational.Integer.integer_defs]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_assoc_l [lemma, in Rational.Integer.PlusZ]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plusZ_simpl_l [axiom, in Rational.Integer.int]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
plus_simpl_l [lemma, in Rational.Natural.NATURAL]
Pos [definition, in Rational.Rational.rational_defs]
Pos [definition, in Rational.Rational.rational_defs]
Pos [definition, in Rational.Rational.rational_defs]
productSyntax [library]
proof [axiom, in Rational.Subset.subset]
proof [axiom, in Rational.Subset.subset]
proof [axiom, in Rational.Subset.subset]
proof [axiom, in Rational.Subset.subset]
proof [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
Prop_closure [axiom, in Rational.Subset.subset]
PX [definition, in Rational.Quotient.extensionality]
PX [definition, in Rational.Quotient.extensionality]

Q

Q [definition, in Rational.Rational.rational_defs]
quotient [library]
Q_typ [definition, in Rational.Rational.rational_defs]
Q_rel [definition, in Rational.Rational.rational_defs]
Q_typ [definition, in Rational.Rational.rational_defs]
Q_rel [definition, in Rational.Rational.rational_defs]
Q_typ [definition, in Rational.Rational.rational_defs]
Q_typ [definition, in Rational.Rational.rational_defs]
Q_typ [definition, in Rational.Rational.rational_defs]
Q_rel [definition, in Rational.Rational.rational_defs]
Q_rel [definition, in Rational.Rational.rational_defs]
Q_rel [definition, in Rational.Rational.rational_defs]

R

rat [section, in Rational.Rational.rat]
rat [section, in Rational.Rational.rat]
rat [section, in Rational.Rational.rat]
rat [library]
rational [library]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
Rationals [section, in Rational.Rational.rational_defs]
rational_defs [library]
Reduce [axiom, in Rational.Quotient.quotient]
Reduce [axiom, in Rational.Quotient.quotient]
Reduce [axiom, in Rational.Quotient.quotient]
Reduce [axiom, in Rational.Quotient.quotient]
Reduce [axiom, in Rational.Quotient.quotient]
Reduce [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reduce_prop [axiom, in Rational.Quotient.quotient]
Reform [definition, in Rational.Quotient.extensionality]
Reform [definition, in Rational.Quotient.extensionality]
Reform [definition, in Rational.Quotient.extensionality]
Reform [definition, in Rational.Quotient.extensionality]
Reform [definition, in Rational.Quotient.extensionality]
Reform [definition, in Rational.Quotient.extensionality]
Rf_is_f [lemma, in Rational.Quotient.extensionality]
Rf_is_f [lemma, in Rational.Quotient.extensionality]
Rf_is_f [lemma, in Rational.Quotient.extensionality]
Rf_is_f [lemma, in Rational.Quotient.extensionality]
Rf_is_f [lemma, in Rational.Quotient.extensionality]
Rf_is_f [lemma, in Rational.Quotient.extensionality]
Rf_is_f [lemma, in Rational.Quotient.extensionality]

S

Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
Set_closure [axiom, in Rational.Subset.subset]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
sign_simpl [lemma, in Rational.Integer.MultZ]
subset [library]
swap [definition, in Rational.Integer.integer_defs]
swap [definition, in Rational.Integer.integer_defs]
swap [definition, in Rational.Integer.integer_defs]
swap [definition, in Rational.Integer.integer_defs]
S1 [lemma, in Rational.Integer.leZproperties]
S1 [lemma, in Rational.Integer.leZproperties]
S2 [lemma, in Rational.Integer.leZproperties]
S2 [lemma, in Rational.Integer.leZproperties]
S3 [lemma, in Rational.Integer.leZproperties]
S3 [lemma, in Rational.Integer.leZproperties]

T

tech1 [lemma, in Rational.Integer.leZ]
tech1 [lemma, in Rational.Integer.leZ]
tech1 [lemma, in Rational.Integer.leZ]
tech1 [lemma, in Rational.Integer.leZ]
tech1 [lemma, in Rational.Integer.leZ]

U

U [definition, in Rational.Quotient.extensionality]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_XX [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minus [definition, in Rational.Integer.integer_defs]
unary_minusQ_X [definition, in Rational.Rational.minus]
unary_minusQ_X [definition, in Rational.Rational.minus]

X

xi [axiom, in Rational.Quotient.extensionality]
xi [axiom, in Rational.Quotient.extensionality]

Z

Z [definition, in Rational.Integer.integer_defs]
Z_partition [lemma, in Rational.Integer.leZproperties]
Z_rel [definition, in Rational.Integer.integer_defs]
z_lt_O [lemma, in Rational.Integer.leZproperties]
z_lt_O [lemma, in Rational.Integer.leZproperties]
Z_partition [lemma, in Rational.Integer.leZproperties]
Z_partition [lemma, in Rational.Integer.leZproperties]
z_eq_O [lemma, in Rational.Integer.leZproperties]
Z_typ [definition, in Rational.Integer.integer_defs]
Z_partition [lemma, in Rational.Integer.leZproperties]
z_lt_O [lemma, in Rational.Integer.leZproperties]
z_lt_O [lemma, in Rational.Integer.leZproperties]
Z_typ [definition, in Rational.Integer.integer_defs]
Z_partition [lemma, in Rational.Integer.leZproperties]
Z_partition [lemma, in Rational.Integer.leZproperties]
z_eq_O [lemma, in Rational.Integer.leZproperties]
Z_typ [definition, in Rational.Integer.integer_defs]
z_eq_O [lemma, in Rational.Integer.leZproperties]
Z_rel [definition, in Rational.Integer.integer_defs]
Z_rel [definition, in Rational.Integer.integer_defs]
z_eq_O [lemma, in Rational.Integer.leZproperties]
z_lt_O [lemma, in Rational.Integer.leZproperties]
Z_partition [lemma, in Rational.Integer.leZproperties]
Z_typ [definition, in Rational.Integer.integer_defs]
Z_rel [definition, in Rational.Integer.integer_defs]
Z_partition [lemma, in Rational.Integer.leZproperties]
Z_partition [lemma, in Rational.Integer.leZproperties]
Z_rel [definition, in Rational.Integer.integer_defs]
Z_partition [lemma, in Rational.Integer.leZproperties]
z_eq_O [lemma, in Rational.Integer.leZproperties]
z_lt_O [lemma, in Rational.Integer.leZproperties]
Z_typ [definition, in Rational.Integer.integer_defs]
z_eq_O [lemma, in Rational.Integer.leZproperties]
Z_partition [lemma, in Rational.Integer.leZproperties]
Z_to_Q [library]

other

_ <= _ (INT_scope) [notation, in Rational.Integer.leZ]
0 (INT_scope) [notation, in Rational.Integer.integer_defs]
_ .2 (INT_scope) [notation, in Rational.Integer.integer_defs]
_ * _ (INT_scope) [notation, in Rational.Integer.integer_defs]
_ < _ (INT_scope) [notation, in Rational.Integer.leZ]
1 (INT_scope) [notation, in Rational.Integer.integer_defs]
- _ (INT_scope) [notation, in Rational.Integer.integer_defs]
_ .2 (INT_scope) [notation, in Rational.Rational.rational_defs]
_ .1 (INT_scope) [notation, in Rational.Rational.rational_defs]
_ .1 (INT_scope) [notation, in Rational.Integer.integer_defs]
_ + _ (INT_scope) [notation, in Rational.Integer.integer_defs]
1 (nat_scope) [notation, in Rational.Natural.NATURAL]
0 (nat_scope) [notation, in Rational.Natural.NATURAL]
_ .2 (nat_scope) [notation, in Rational.Natural.NATURAL]
_ .1 (nat_scope) [notation, in Rational.Natural.NATURAL]
- _ (RAT_scope) [notation, in Rational.Rational.minus]
_ + _ (RAT_scope) [notation, in Rational.Rational.rational_defs]
_ * _ (RAT_scope) [notation, in Rational.Rational.rational_defs]
_ ^2 [notation, in Rational.Util.productSyntax]
_ / _ [notation, in Rational.Quotient.quotient]
_ = _ [notation, in Rational.Natural.NATURAL]
_ ^1 [notation, in Rational.Util.productSyntax]
_ ! _ [notation, in Rational.Subset.subset]
%+ _ _ [notation, in Rational.Rational.rational_defs]
%+ _ [notation, in Rational.Subset.subset]
%- _ [notation, in Rational.Rational.rational_defs]
| _ | z [notation, in Rational.Integer.integer_defs]
| _ | q [notation, in Rational.Rational.rational_defs]
| _ | [notation, in Rational.Quotient.quotient]

Notation Index

I

_ + _ (INT_scope) [in Rational.Integer.integer_defs]

L

_ <= _ (INT_scope) [in Rational.Integer.leZ]

other

_ <= _ (INT_scope) [in Rational.Integer.leZ]
0 (INT_scope) [in Rational.Integer.integer_defs]
_ .2 (INT_scope) [in Rational.Integer.integer_defs]
_ * _ (INT_scope) [in Rational.Integer.integer_defs]
_ < _ (INT_scope) [in Rational.Integer.leZ]
1 (INT_scope) [in Rational.Integer.integer_defs]
- _ (INT_scope) [in Rational.Integer.integer_defs]
_ .2 (INT_scope) [in Rational.Rational.rational_defs]
_ .1 (INT_scope) [in Rational.Rational.rational_defs]
_ .1 (INT_scope) [in Rational.Integer.integer_defs]
_ + _ (INT_scope) [in Rational.Integer.integer_defs]
1 (nat_scope) [in Rational.Natural.NATURAL]
0 (nat_scope) [in Rational.Natural.NATURAL]
_ .2 (nat_scope) [in Rational.Natural.NATURAL]
_ .1 (nat_scope) [in Rational.Natural.NATURAL]
- _ (RAT_scope) [in Rational.Rational.minus]
_ + _ (RAT_scope) [in Rational.Rational.rational_defs]
_ * _ (RAT_scope) [in Rational.Rational.rational_defs]
_ ^2 [in Rational.Util.productSyntax]
_ / _ [in Rational.Quotient.quotient]
_ = _ [in Rational.Natural.NATURAL]
_ ^1 [in Rational.Util.productSyntax]
_ ! _ [in Rational.Subset.subset]
%+ _ _ [in Rational.Rational.rational_defs]
%+ _ [in Rational.Subset.subset]
%- _ [in Rational.Rational.rational_defs]
| _ | z [in Rational.Integer.integer_defs]
| _ | q [in Rational.Rational.rational_defs]
| _ | [in Rational.Quotient.quotient]

Variable Index

E

Extensionality.A [in Rational.Quotient.extensionality]
Extensionality.B [in Rational.Quotient.extensionality]

Library Index

A

Absz
AC

E

H

I

int
integer
integer_defs
intnumbers

L

leZ
leZproperties

M

minus
MultQ
MultZ

N

P

PlusQ
PlusZ
productSyntax

Q

R

rat
rational
rational_defs

S

subset

Z

Z_to_Q

Lemma Index

A

ABSZ [in Rational.Integer.Absz]
ABSZ [in Rational.Integer.Absz]
ABSZ [in Rational.Integer.Absz]
ABSZ [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]
ABSZ_O [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_O [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]
ABSZ_O [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_O [in Rational.Integer.Absz]
ABSZ_O [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_O [in Rational.Integer.Absz]
ABSZ_neg [in Rational.Integer.Absz]
ABSZ_pos [in Rational.Integer.Absz]

C

Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_PX [in Rational.Quotient.extensionality]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_swap [in Rational.Integer.integer_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_PX [in Rational.Quotient.extensionality]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_swap [in Rational.Integer.integer_defs]
Compat_PX [in Rational.Quotient.extensionality]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_swap [in Rational.Integer.integer_defs]
Compat_PX [in Rational.Quotient.extensionality]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_swap [in Rational.Integer.integer_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_PX [in Rational.Quotient.extensionality]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_PX [in Rational.Quotient.extensionality]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_PX [in Rational.Quotient.extensionality]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_swap [in Rational.Integer.integer_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_PX [in Rational.Quotient.extensionality]
Compat_swap [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_swap [in Rational.Integer.integer_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_multZ_XX [in Rational.Integer.integer_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_swap [in Rational.Integer.integer_defs]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_swap [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_PX [in Rational.Quotient.extensionality]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_leZ_X [in Rational.Integer.leZ]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_multZ_X [in Rational.Integer.integer_defs]
Compat_multQ_XX [in Rational.Rational.rational_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_swap [in Rational.Integer.integer_defs]
Compat_plusZ_XX [in Rational.Integer.integer_defs]
Compat_unary_minusQ_X [in Rational.Rational.minus]
Compat_swap [in Rational.Integer.integer_defs]
Compat_multQ_X [in Rational.Rational.rational_defs]
Compat_plusQ_X [in Rational.Rational.rational_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_plusQ_XX [in Rational.Rational.rational_defs]
Compat_plusZ_X [in Rational.Integer.integer_defs]
Compat_leZ_XX [in Rational.Integer.leZ]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]
Constructive_Z_partition [in Rational.Integer.leZproperties]

D

distribQ [in Rational.Rational.MultQ]
distribQ [in Rational.Rational.MultQ]
distribQ [in Rational.Rational.MultQ]
distribQ [in Rational.Rational.MultQ]
distribQ [in Rational.Rational.MultQ]
distribQ [in Rational.Rational.MultQ]
distribQ [in Rational.Rational.MultQ]
distribQ [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribQ_l [in Rational.Rational.MultQ]
distribZ [in Rational.Integer.MultZ]
distribZ [in Rational.Integer.MultZ]
distribZ [in Rational.Integer.MultZ]
distribZ [in Rational.Integer.MultZ]
distribZ [in Rational.Integer.MultZ]
distribZ [in Rational.Integer.MultZ]
distribZ [in Rational.Integer.MultZ]
distribZ [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]
distribZ_l [in Rational.Integer.MultZ]

E

eq_pair [in Rational.Integer.integer_defs]
eq_pair [in Rational.Integer.integer_defs]
eq_pair [in Rational.Integer.integer_defs]
eq_pair [in Rational.Integer.integer_defs]
eq_pair [in Rational.Integer.integer_defs]
eq_pair [in Rational.Integer.integer_defs]
eq_pair [in Rational.Integer.integer_defs]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]
extensionality [in Rational.Quotient.extensionality]

L

le_with_plus2 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_false [in Rational.Integer.leZproperties]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_false [in Rational.Integer.leZproperties]
le_false [in Rational.Integer.leZproperties]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_false [in Rational.Integer.leZproperties]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_false [in Rational.Integer.leZproperties]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus1 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_with_plus2 [in Rational.Integer.leZ]
le_false [in Rational.Integer.leZproperties]
le_with_plus1 [in Rational.Integer.leZ]
le_false [in Rational.Integer.leZproperties]
le_false [in Rational.Integer.leZproperties]

M

multQ_sym [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_simpl_l [in Rational.Rational.rat]
multQ_permute [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_sym [in Rational.Rational.MultQ]
multQ_sym [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_sym [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_permute [in Rational.Rational.MultQ]
multQ_sym [in Rational.Rational.MultQ]
multQ_sym [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_sym [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_simpl_l [in Rational.Rational.rat]
multQ_sym [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_permute [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_simpl_l [in Rational.Rational.rat]
multQ_simpl_l [in Rational.Rational.rat]
multQ_sym [in Rational.Rational.MultQ]
multQ_assoc_l [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multQ_assoc_r [in Rational.Rational.MultQ]
multQ_permute [in Rational.Rational.MultQ]
multZ_permute [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_O [in Rational.Integer.MultZ]
multZ_O [in Rational.Integer.MultZ]
multZ_O [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_O [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_O [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_sym [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_O [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_O [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_permute [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_r [in Rational.Integer.MultZ]
multZ_assoc_l [in Rational.Integer.MultZ]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_permute [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_plus_distr_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]
mult_simpl_l [in Rational.Natural.NATURAL]

O

one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
one_is_a_denominator [in Rational.Rational.Z_to_Q]
O_lt_z [in Rational.Integer.leZproperties]
O_lt_z [in Rational.Integer.leZproperties]
O_lt_z [in Rational.Integer.leZproperties]
O_lt_z [in Rational.Integer.leZproperties]
O_lt_z [in Rational.Integer.leZproperties]
O_lt_z [in Rational.Integer.leZproperties]

P

plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_sym [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_assoc_l [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusQ_permute [in Rational.Rational.PlusQ]
plusQ_assoc_r [in Rational.Rational.PlusQ]
plusQ_simpl_l [in Rational.Rational.rat]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_O [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_O [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_O [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_O [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_O [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_O [in Rational.Integer.PlusZ]
plusZ_O [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_plus_l [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_sym [in Rational.Integer.PlusZ]
plusZ_permute [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_assoc_r [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plusZ_assoc_l [in Rational.Integer.PlusZ]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]
plus_simpl_l [in Rational.Natural.NATURAL]

R

Rf_is_f [in Rational.Quotient.extensionality]
Rf_is_f [in Rational.Quotient.extensionality]
Rf_is_f [in Rational.Quotient.extensionality]
Rf_is_f [in Rational.Quotient.extensionality]
Rf_is_f [in Rational.Quotient.extensionality]
Rf_is_f [in Rational.Quotient.extensionality]
Rf_is_f [in Rational.Quotient.extensionality]

S

sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
sign_simpl [in Rational.Integer.MultZ]
S1 [in Rational.Integer.leZproperties]
S1 [in Rational.Integer.leZproperties]
S2 [in Rational.Integer.leZproperties]
S2 [in Rational.Integer.leZproperties]
S3 [in Rational.Integer.leZproperties]
S3 [in Rational.Integer.leZproperties]

T

tech1 [in Rational.Integer.leZ]
tech1 [in Rational.Integer.leZ]
tech1 [in Rational.Integer.leZ]
tech1 [in Rational.Integer.leZ]
tech1 [in Rational.Integer.leZ]

Z

Z_partition [in Rational.Integer.leZproperties]
z_lt_O [in Rational.Integer.leZproperties]
z_lt_O [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
z_eq_O [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
z_lt_O [in Rational.Integer.leZproperties]
z_lt_O [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
z_eq_O [in Rational.Integer.leZproperties]
z_eq_O [in Rational.Integer.leZproperties]
z_eq_O [in Rational.Integer.leZproperties]
z_lt_O [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]
z_eq_O [in Rational.Integer.leZproperties]
z_lt_O [in Rational.Integer.leZproperties]
z_eq_O [in Rational.Integer.leZproperties]
Z_partition [in Rational.Integer.leZproperties]

Axiom Index

C

Canonic [in Rational.Subset.subset]
Canonic [in Rational.Subset.subset]
Canonic [in Rational.Subset.subset]
Canonic [in Rational.Subset.subset]
Canonic [in Rational.Subset.subset]
Canonic [in Rational.Subset.subset]
Canonic [in Rational.Subset.subset]
Closure [in Rational.Quotient.quotient]
Closure [in Rational.Quotient.quotient]
Closure [in Rational.Quotient.quotient]
Closure [in Rational.Quotient.quotient]
Closure [in Rational.Quotient.quotient]
Closure [in Rational.Quotient.quotient]
Closure [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]
Closure_prop [in Rational.Quotient.quotient]

E

Ext [in Rational.Quotient.quotient]
Ext [in Rational.Quotient.quotient]
Ext [in Rational.Quotient.quotient]

F

From_R_to_L [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_R_to_L [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]
From_L_to_R [in Rational.Quotient.quotient]

I

In [in Rational.Quotient.quotient]
In [in Rational.Quotient.quotient]
In_subset [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_Out [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_Out [in Rational.Subset.subset]
In_Out [in Rational.Subset.subset]
In_Out [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_Out [in Rational.Subset.subset]
In_subset [in Rational.Subset.subset]
In_Out [in Rational.Subset.subset]

L

lift [in Rational.Quotient.quotient]
lift [in Rational.Quotient.quotient]
lift [in Rational.Quotient.quotient]
lift [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]
lift_prop [in Rational.Quotient.quotient]

M

MK_SUBSET [in Rational.Subset.subset]
MK_SUBSET [in Rational.Subset.subset]
MK_QUO [in Rational.Quotient.quotient]
MK_QUO [in Rational.Quotient.quotient]
MK_QUO [in Rational.Quotient.quotient]
MK_SUBSET [in Rational.Subset.subset]
MK_SUBSET [in Rational.Subset.subset]
MK_SUBSET [in Rational.Subset.subset]
MK_QUO [in Rational.Quotient.quotient]
MK_SUBSET [in Rational.Subset.subset]
MK_QUO [in Rational.Quotient.quotient]
MK_SUBSET [in Rational.Subset.subset]
MK_SUBSET [in Rational.Subset.subset]
MK_QUO [in Rational.Quotient.quotient]
MK_SUBSET [in Rational.Subset.subset]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
multZ_simpl_l [in Rational.Integer.int]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]
mult_minus [in Rational.Integer.MultZ]

O

Out_subset [in Rational.Subset.subset]
Out_In [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_In [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_In [in Rational.Subset.subset]
Out_In [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_In [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]
Out_In [in Rational.Subset.subset]
Out_subset [in Rational.Subset.subset]

P

plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusQ_plus_l [in Rational.Rational.PlusQ]
plusQ_XXX_prelim [in Rational.Rational.rational_defs]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
plusZ_simpl_l [in Rational.Integer.int]
proof [in Rational.Subset.subset]
proof [in Rational.Subset.subset]
proof [in Rational.Subset.subset]
proof [in Rational.Subset.subset]
proof [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]
Prop_closure [in Rational.Subset.subset]

R

Reduce [in Rational.Quotient.quotient]
Reduce [in Rational.Quotient.quotient]
Reduce [in Rational.Quotient.quotient]
Reduce [in Rational.Quotient.quotient]
Reduce [in Rational.Quotient.quotient]
Reduce [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]
Reduce_prop [in Rational.Quotient.quotient]

S

Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]
Set_closure [in Rational.Subset.subset]

X

xi [in Rational.Quotient.extensionality]
xi [in Rational.Quotient.extensionality]

Constructor Index

E

EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]
EXP_intro [in Rational.Integer.leZproperties]

Inductive Index

E

EXP [in Rational.Integer.leZproperties]
EXP [in Rational.Integer.leZproperties]
EXP [in Rational.Integer.leZproperties]

Section Index

A

AbsZ [in Rational.Integer.Absz]
AbsZ [in Rational.Integer.Absz]
AbsZ [in Rational.Integer.Absz]
AbsZ [in Rational.Integer.Absz]

B

binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]
binary_minus [in Rational.Rational.minus]

E

Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]
Extensionality [in Rational.Quotient.extensionality]

I

INT [in Rational.Integer.int]
INT [in Rational.Integer.int]
INT [in Rational.Integer.int]
Integers [in Rational.Integer.integer_defs]
Integers [in Rational.Integer.integer_defs]
Integers [in Rational.Integer.integer_defs]
Integers [in Rational.Integer.integer_defs]
Integers [in Rational.Integer.integer_defs]
Integers [in Rational.Integer.integer_defs]
Integers [in Rational.Integer.integer_defs]
Integers [in Rational.Integer.integer_defs]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]
Integers_are_Rationals [in Rational.Rational.Z_to_Q]

L

LEZ [in Rational.Integer.leZ]
LEZ [in Rational.Integer.leZ]
LEZ [in Rational.Integer.leZ]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]
leZproperties [in Rational.Integer.leZproperties]

M

minus [in Rational.Rational.minus]
minus [in Rational.Rational.minus]
minus [in Rational.Rational.minus]
minus [in Rational.Rational.minus]
minus [in Rational.Rational.minus]
MultQ [in Rational.Rational.MultQ]
MultQ [in Rational.Rational.MultQ]
MultQ [in Rational.Rational.MultQ]
MultQ [in Rational.Rational.MultQ]
MultQ [in Rational.Rational.MultQ]
MultZ [in Rational.Integer.MultZ]
MultZ [in Rational.Integer.MultZ]
MultZ [in Rational.Integer.MultZ]
MultZ [in Rational.Integer.MultZ]
MultZ [in Rational.Integer.MultZ]

N

NAT [in Rational.Natural.NATURAL]
NAT [in Rational.Natural.NATURAL]
NAT [in Rational.Natural.NATURAL]

P

plusQ [in Rational.Rational.PlusQ]
plusQ [in Rational.Rational.PlusQ]
plusQ [in Rational.Rational.PlusQ]
plusQ [in Rational.Rational.PlusQ]
plusQ [in Rational.Rational.PlusQ]
PlusZ [in Rational.Integer.PlusZ]
PlusZ [in Rational.Integer.PlusZ]
PlusZ [in Rational.Integer.PlusZ]
PlusZ [in Rational.Integer.PlusZ]
PlusZ [in Rational.Integer.PlusZ]

R

rat [in Rational.Rational.rat]
rat [in Rational.Rational.rat]
rat [in Rational.Rational.rat]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]
Rationals [in Rational.Rational.rational_defs]

Definition Index

B

binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]
binary_minusQ [in Rational.Rational.minus]

C

Compat [in Rational.Quotient.quotient]
Compat [in Rational.Quotient.quotient]
Compat [in Rational.Quotient.quotient]
Compat [in Rational.Quotient.quotient]
Compat [in Rational.Quotient.quotient]
Compat [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]
Compat_prop [in Rational.Quotient.quotient]

E

E [in Rational.Quotient.extensionality]
eq_ext [in Rational.Quotient.extensionality]
eq_ext [in Rational.Quotient.extensionality]
eq_ext [in Rational.Quotient.extensionality]
eq_ext [in Rational.Quotient.extensionality]
eq_ext [in Rational.Quotient.extensionality]
eq_ext [in Rational.Quotient.extensionality]

F

fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]
fromZ_to_Q [in Rational.Rational.Z_to_Q]

L

leZ [in Rational.Integer.leZ]
leZ [in Rational.Integer.leZ]
leZ [in Rational.Integer.leZ]
leZ_XX [in Rational.Integer.leZ]
leZ_XX [in Rational.Integer.leZ]
leZ_XX [in Rational.Integer.leZ]
leZ_XX [in Rational.Integer.leZ]
leZ_XX [in Rational.Integer.leZ]
leZ_X [in Rational.Integer.leZ]
leZ_X [in Rational.Integer.leZ]
leZ_XX [in Rational.Integer.leZ]
leZ_X [in Rational.Integer.leZ]
leZ_X [in Rational.Integer.leZ]
leZ_X [in Rational.Integer.leZ]
ltZ [in Rational.Integer.leZ]
ltZ [in Rational.Integer.leZ]
ltZ [in Rational.Integer.leZ]

M

multQ [in Rational.Rational.rational_defs]
multQ [in Rational.Rational.rational_defs]
multQ [in Rational.Rational.rational_defs]
multQ [in Rational.Rational.rational_defs]
multQ [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_X [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multQ_X [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_X [in Rational.Rational.rational_defs]
multQ_X [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_X [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multQ_X [in Rational.Rational.rational_defs]
multQ_XXX [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multQ_X [in Rational.Rational.rational_defs]
multQ_XX [in Rational.Rational.rational_defs]
multZ [in Rational.Integer.integer_defs]
multZ [in Rational.Integer.integer_defs]
multZ [in Rational.Integer.integer_defs]
multZ [in Rational.Integer.integer_defs]
multZ [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_X [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]
multZ_X [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]
multZ_X [in Rational.Integer.integer_defs]
multZ_X [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]
multZ_XXX [in Rational.Integer.integer_defs]
multZ_X [in Rational.Integer.integer_defs]
multZ_X [in Rational.Integer.integer_defs]
multZ_X [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]
multZ_XX [in Rational.Integer.integer_defs]

P

P [in Rational.Quotient.extensionality]
plusQ [in Rational.Rational.rational_defs]
plusQ [in Rational.Rational.rational_defs]
plusQ [in Rational.Rational.rational_defs]
plusQ [in Rational.Rational.rational_defs]
plusQ [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_X [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_X [in Rational.Rational.rational_defs]
plusQ_X [in Rational.Rational.rational_defs]
plusQ_X [in Rational.Rational.rational_defs]
plusQ_XX [in Rational.Rational.rational_defs]
plusQ_X [in Rational.Rational.rational_defs]
plusQ_X [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_XXX [in Rational.Rational.rational_defs]
plusQ_X [in Rational.Rational.rational_defs]
plusZ [in Rational.Integer.integer_defs]
plusZ [in Rational.Integer.integer_defs]
plusZ [in Rational.Integer.integer_defs]
plusZ [in Rational.Integer.integer_defs]
plusZ [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_X [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_X [in Rational.Integer.integer_defs]
plusZ_X [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_X [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_X [in Rational.Integer.integer_defs]
plusZ_XX [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
plusZ_X [in Rational.Integer.integer_defs]
plusZ_X [in Rational.Integer.integer_defs]
plusZ_XXX [in Rational.Integer.integer_defs]
Pos [in Rational.Rational.rational_defs]
Pos [in Rational.Rational.rational_defs]
Pos [in Rational.Rational.rational_defs]
PX [in Rational.Quotient.extensionality]
PX [in Rational.Quotient.extensionality]

Q

Q [in Rational.Rational.rational_defs]
Q_typ [in Rational.Rational.rational_defs]
Q_rel [in Rational.Rational.rational_defs]
Q_typ [in Rational.Rational.rational_defs]
Q_rel [in Rational.Rational.rational_defs]
Q_typ [in Rational.Rational.rational_defs]
Q_typ [in Rational.Rational.rational_defs]
Q_typ [in Rational.Rational.rational_defs]
Q_rel [in Rational.Rational.rational_defs]
Q_rel [in Rational.Rational.rational_defs]
Q_rel [in Rational.Rational.rational_defs]

R

Reform [in Rational.Quotient.extensionality]
Reform [in Rational.Quotient.extensionality]
Reform [in Rational.Quotient.extensionality]
Reform [in Rational.Quotient.extensionality]
Reform [in Rational.Quotient.extensionality]
Reform [in Rational.Quotient.extensionality]

S

swap [in Rational.Integer.integer_defs]
swap [in Rational.Integer.integer_defs]
swap [in Rational.Integer.integer_defs]
swap [in Rational.Integer.integer_defs]

U

U [in Rational.Quotient.extensionality]
unary_minusQ_X [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_XX [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]
unary_minus [in Rational.Integer.integer_defs]
unary_minusQ_X [in Rational.Rational.minus]
unary_minusQ_X [in Rational.Rational.minus]

Z

Z [in Rational.Integer.integer_defs]
Z_rel [in Rational.Integer.integer_defs]
Z_typ [in Rational.Integer.integer_defs]
Z_typ [in Rational.Integer.integer_defs]
Z_typ [in Rational.Integer.integer_defs]
Z_rel [in Rational.Integer.integer_defs]
Z_rel [in Rational.Integer.integer_defs]
Z_typ [in Rational.Integer.integer_defs]
Z_rel [in Rational.Integer.integer_defs]
Z_rel [in Rational.Integer.integer_defs]
Z_typ [in Rational.Integer.integer_defs]

Global Index

G

J

K

V

W

Y

_

(1380 entries)

Notation Index

A

B

C

D

E

F

G

H

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(31 entries)

Variable Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Library Index

B

C

D

F

G

J

K

O

T

U

V

W

X

Y

_

other

(25 entries)

Lemma Index

B

F

G

H

I

J

K

N

Q

U

V

W

X

Y

_

other

(697 entries)

Axiom Index

A

B

D

G

H

J

K

N

Q

T

U

V

W

Y

Z

_

other

(223 entries)

Constructor Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Inductive Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Section Index

C

D

F

G

H

J

K

O

Q

S

T

U

V

W

X

Y

Z

_

other

(119 entries)

Definition Index

A

D

G

H

I

J

K

N

O

T

V

W

X

Y

_

other

(271 entries)