Moved some lemmas from fpmod to CoqEAL