compreal is_distributive_wrt addreal by Th8, Th9, FINSEQOP:63;