Step
*
of Lemma
iseg_product_rem_property
∀[k,j:ℕ]. ∀[i:ℕj + 1]. iseg_product_rem(i;j;k) = (iseg_product(i;j) rem k) ∈ ℤ supposing 1 < k
BY
{ xxx(Auto
THEN RepUR ``iseg_product_rem iseg_product combinations`` 0
THEN (RWO "combinations_aux_rem_property<" 0 THENM EqCD)
THEN Auto')xxx }
Latex:
Latex:
\mforall{}[k,j:\mBbbN{}]. \mforall{}[i:\mBbbN{}j + 1]. iseg\_product\_rem(i;j;k) = (iseg\_product(i;j) rem k) supposing 1 < k
By
Latex:
xxx(Auto
THEN RepUR ``iseg\_product\_rem iseg\_product combinations`` 0
THEN (RWO "combinations\_aux\_rem\_property<" 0 THENM EqCD)
THEN Auto')xxx
Home
Index