proposition: Lemma preserves_dec_recip `{IsDecField F2} `{forall x y: F2, Decidable (x = y)} `{!IsSemiRingPreserving (f : F -> F2)} x : f (/ x) = / f x.
proof: Proof. case (dec (x = 0)) as [E | E]. - rewrite E, dec_recip_0, preserves_0, dec_recip_0. reflexivity. - intros. apply (left_cancellation_ne_0 (.*.) (f x)). + apply isinjective_ne_0. trivial. + rewrite <-preserves_mult, 2!dec_recip_inverse. * apply preserves_1. * apply isinjective_ne_0. trivial. * trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.fields HoTT.Classes.theory.apartness HoTT.Classes.theory.rings