for a being NAT -valued Real_Sequence
for b being non trivial Nat st rng a c= b & a is eventually-non-zero holds
Liouville_constant (a,b) is liouville