SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
a
,
b
,
c
,
d
:
.
a
=
b
c
=
d
a
c
=
d
b
[mul_nat_com]
cites the following:
1
Thm*
a
,
b
:
. 0
a
b
[mul_bounds_1a]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
SimpleMulFacts
Sections
DiscrMathExt
Doc
a,b,c,d:
. a = b 
c = d a
c = db 
a,b:. 0
aba,b,c,d:. a = b c = d ac = db a,b:. 0ab