proposition: Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R.
proof: Proof. unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. - simpl; intros; elim H; trivial. - intros; field; auto. - intros; change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R; change (IZR (Zneg p)) with (- IZR (Zpos p))%R; simpl; field; repeat split; auto; auto with real. Qed.
imports: Rdefinitions Raxioms RIneq QArith_base