Def  b | a == c:. a = bc

is mentioned by

Thm*  a,b:, e:({a..b}), i:{a..b}. e(i) | ( i:{a..b}. e(i))

[components_divide_iter_mul]

In prior sections: num thy 1 SimpleMulFacts

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html