Implemented part of Lemma 4.2 (is_fplusq_evalid function), and added asset
to be nat.