diff options
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/Qcanon.v | 4 | ||||
| -rw-r--r-- | theories/QArith/Qreals.v | 7 |
2 files changed, 5 insertions, 6 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index e395e4d03..e777c74d3 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -460,13 +460,13 @@ Proof. induction n; simpl; auto with qarith. rewrite IHn; auto with qarith. Qed. - +Transparent Qred. Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0. Proof. destruct n; simpl. destruct 1; auto. intros. - now apply Qc_is_canon. + now apply Qc_is_canon. Qed. Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 4a826f691..f363fd7c2 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -167,14 +167,13 @@ Qed. Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R. Proof. -unfold Qinv, Q2R, Qeq; intros (x1, x2); unfold Qden, Qnum. -case x1. +unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. simpl; intros; elim H; trivial. -intros; field; auto. +intros; field; auto. intros; change (IZR (Zneg x2)) with (- IZR (' x2))%R; change (IZR (Zneg p)) with (- IZR (' p))%R; - field; (*auto 8 with real.*) + simpl; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. |