proposition: Lemma CRinv_mult_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R) (r1nz : r1 ≶ 0) (r2nz : r2 ≶ 0) (rmnz : (r1*r2) ≶ 0), (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.
proof: Proof. intros. apply (CRmult_eq_reg_l r1). - exact r1nz. - rewrite (Rmul_assoc (CRisRing R)). rewrite CRinv_r. rewrite CRmult_1_l. apply (CRmult_eq_reg_l r2). + exact r2nz. + rewrite CRinv_r. rewrite (Rmul_assoc (CRisRing R)). rewrite (CRmult_comm r2 r1). rewrite CRinv_r. reflexivity. Qed.
imports: QArith Qabs Qround