proposition: Theorem Rinv_Rdiv_depr : forall x y:R, x <> 0 -> y <> 0 -> / (x / y) = y / x.
proof: Proof. intros x y _ _. apply Rinv_div. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra