proposition: Lemma Rinv_mult_simpl_depr : forall r1 r2 r3, r1 <> 0 -> r1 * / r2 * (r3 * / r1) = r3 * / r2.
proof: Proof. intros r1 r2 r3 r1n0. rewrite (Rmult_comm r3 (/ r1)), Rmult_assoc, <-(Rmult_assoc (/ r2)). rewrite (Rmult_comm r3), (Rmult_comm (/ r2)), <-2Rmult_assoc. now rewrite Rinv_r, Rmult_1_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField