diff options
| author | Vincent Semeria | 2019-06-27 23:35:03 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2019-07-16 18:45:34 +0200 |
| commit | eebc676ce4978b7e408c427889bae356d8b0efdc (patch) | |
| tree | 2bc6228c80817026d4e2108e871867fc50a86fa2 /theories/QArith | |
| parent | 3bd2722fb53552f45a25e6bc0a03a9ab0517485f (diff) | |
Define constructive real numbers as Cauchy sequences of rational numbers. Redefine classical real numbers as a quotient of those constructive real numbers.
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith_base.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 3a613c55ec..21bea6c315 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -562,6 +562,16 @@ Proof. apply Qdiv_mult_l; auto. Qed. +Lemma Qinv_plus_distr : forall a b c, ((a # c) + (b # c) == (a+b) # c)%Q. +Proof. + intros. unfold Qeq. simpl. rewrite Pos2Z.inj_mul. ring. +Qed. + +Lemma Qinv_minus_distr : forall a b c, (a # c) + - (b # c) == (a-b) # c. +Proof. + intros. unfold Qeq. simpl. rewrite Pos2Z.inj_mul. ring. +Qed. + (** Injectivity of Qmult (requires theory about Qinv above): *) Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y). |