add initial f16 fadd formal proof