`{IsField F2} `{!IsSemiRingStrongPreserving (f : F -> F2)} x Pfx : f (/ x) = // (f x;Pfx). Proof. assert (x <> 0). - intros Ex. destruct (apart_ne (f x) 0 Pfx). rewrite Ex, (preserves_0 (f:=f)). reflexivity. - apply (left_cancellation_ne_0 (.*.) (f x)). + apply isinjective_ne_0. trivial. + rewrite <-preserves_mult, dec_recip_inverse, reciperse_alt by assumption. apply preserves_1. Qed.
Require Import