(a b c d : F) : b <> 0 -> d <> 0 -> (a * d = c * b <-> a / b = c / d). Proof. split; intro E. - apply (right_cancellation_ne_0 (.*.) b);trivial. apply (right_cancellation_ne_0 (.*.) d);trivial. transitivity (a * d * (b * /b));[| transitivity (c * b * (d * /d))]. + rewrite <-!(mult_assoc a). apply ap. rewrite (mult_comm d), (mult_comm _ b). reflexivity. + rewrite E, dec_recip_inverse, dec_recip_inverse;trivial. + rewrite <-!(mult_assoc c). apply ap. rewrite (mult_comm d), mult_assoc, (mult_comm b). reflexivity. - transitivity (a * d * 1);[rewrite mult_1_r;reflexivity|]. rewrite <-(dec_recip_inverse b);trivial. transitivity (c * b * 1);[|rewrite mult_1_r;reflexivity]. rewrite <-(dec_recip_inverse d);trivial. rewrite mult_comm, <-mult_assoc, (mult_assoc _ a), (mult_comm _ a), E. rewrite <-mult_assoc. rewrite (mult_comm _ d). rewrite mult_assoc, (mult_comm c). reflexivity. Qed.
Require Import