proposition: Lemma CReal_inv_mult_distr : forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0), (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.
proof: Proof. intros. apply (CReal_mult_eq_reg_l r1). - exact r1nz. - rewrite <- CReal_mult_assoc. rewrite CReal_inv_r. rewrite CReal_mult_1_l. apply (CReal_mult_eq_reg_l r2). + exact r2nz. + rewrite CReal_inv_r. rewrite <- CReal_mult_assoc. rewrite (CReal_mult_comm r2 r1). rewrite CReal_inv_r. reflexivity. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra