@DecField F Fe Fplus Fmult Fzero Fone Fnegate Frecip. Proof with auto. destruct ftheory. repeat (constructor; try assumption); repeat intro ; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op, one_is_mon_unit, mult_is_sg_op, plus, mult, recip, negate; try field. unfold recip, mult. simpl. assert (Fe (Fmult x (Frecip x)) (Fmult (Frecip x) x)) as E by ring. rewrite E. Qed.
Require Import