diff options
| author | Vincent Semeria | 2019-08-09 23:50:19 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2019-08-09 23:50:19 +0200 |
| commit | 0ea914c66097f04784a67999457bf3a6273dff1e (patch) | |
| tree | 4dc49b0d4aac4fe19f156feaf7108f2d054714c0 /theories/QArith | |
| parent | bf35f5534f21c084921b5fc3a0830d4a1d9ebd87 (diff) | |
Switch constructive Rlt to sort Type, to make it compute later
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith_base.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a5ea5cc6e5..b60feb9256 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -728,18 +728,18 @@ Defined. Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }. Proof. - intros. destruct q as [a b]. unfold Qlt. simpl. - rewrite Zmult_1_r. destruct a. + intros. destruct q as [a b]. destruct a. - exists xH. reflexivity. - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))). - apply Z.lt_succ_diag_r. rewrite Pos2Z.inj_mul. + simpl. rewrite Pos.mul_1_r. + apply Z.lt_succ_diag_r. simpl. rewrite Pos2Z.inj_mul. rewrite <- (Zmult_1_r (Z.pos (p+1))). apply Z.mul_le_mono_nonneg. discriminate. rewrite Zmult_1_r. apply Z.le_refl. discriminate. apply Z2Nat.inj_le. discriminate. apply Pos2Z.is_nonneg. apply Nat.le_succ_l. apply Nat2Z.inj_lt. rewrite Z2Nat.id. apply Pos2Z.is_pos. apply Pos2Z.is_nonneg. - exists xH. reflexivity. -Qed. +Defined. (** Compatibility of operations with respect to order. *) |