(x y: F): / (x * y) = / x * / y. Proof. destruct (dec (x = 0)) as [Ex|Ex]. - rewrite Ex, left_absorb, dec_recip_0. apply symmetry,mult_0_l. - destruct (dec (y = 0)) as [Ey|Ey]. + rewrite Ey, dec_recip_0, !mult_0_r. apply dec_recip_0. + assert (x * y <> 0) as Exy by (apply mult_ne_0;trivial). apply (left_cancellation_ne_0 (.*.) (x * y)); trivial. transitivity (x / x * (y / y)). * rewrite !dec_recip_inverse by assumption. rewrite mult_1_l;apply reflexivity. * rewrite !dec_recip_inverse by assumption. rewrite mult_assoc, (mult_comm x), <-(mult_assoc y). rewrite dec_recip_inverse by assumption. rewrite (mult_comm y), <-mult_assoc. rewrite dec_recip_inverse by assumption. reflexivity. Qed.
Require Import