proposition: Lemma Q2R_inv_ext : forall x, Q2R (/ x) = (if Qeq_bool x 0 then 0 else / Q2R x).
proof: Proof. intros. case_eq (Qeq_bool x 0). - intros. apply Qeq_bool_eq in H. destruct x ; simpl. unfold Qeq in H. simpl in H. rewrite Zmult_1_r in H. rewrite H. apply Rmult_0_l. - intros. now apply Q2R_inv, Qeq_bool_neq. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant