proposition: Lemma Rinv_mult r1 r2 : / (r1 * r2) = / r1 * / r2.
proof: Proof. destruct (Req_dec r1 0) as [-> | H1]. - now rewrite Rinv_0, 2!Rmult_0_l, Rinv_0. - destruct (Req_dec r2 0) as [-> | H2]. + now rewrite Rinv_0, 2!Rmult_0_r, Rinv_0. + symmetry; apply Rmult_inv_r_uniq. { now apply Rmult_integral_contrapositive_currified. } rewrite (Rmult_comm r1), Rmult_assoc, <-(Rmult_assoc r1). now rewrite Rinv_r, Rmult_1_l, Rinv_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField