for m being CR_Sequence
for c being CR_coefficients of m
for i being Nat st i in dom c holds
c . i,1 are_congruent_mod m . i