SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
a
,
b
:
,
m
,
n
:
.
m
=
n
(
m
a
=
n
b
a
=
b
)
[mul_cancel_in_eq2]
cites the following:
3
Thm*
a
,
b
:
,
n
:
.
n
a
=
n
b
a
=
b
[mul_cancel_in_eq]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
SimpleMulFacts
Sections
DiscrMathExt
Doc
a,b:
, m,n:
. m = n 
(m
a = nb 
a = b)a,b:, n:. na = nb a = ba,b:, m,n:. m = n (ma = nb a = b)a,b:, n:. na = nb a = b