diff options
Diffstat (limited to 'plugins/micromega/ZCoeff.v')
| -rw-r--r-- | plugins/micromega/ZCoeff.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index 2bf3d8c3..e30295e6 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -109,7 +109,7 @@ Qed. Lemma Zring_morph : ring_morph 0 1 rplus rtimes rminus ropp req - 0%Z 1%Z Zplus Zmult Zminus Zopp + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool gen_order_phi_Z. Proof. exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)). @@ -122,7 +122,7 @@ try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_ try apply (Rlt_0_1 sor); assumption. Qed. -Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Psucc x) == 1 + phi_pos1 x. +Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x. Proof. exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))). @@ -130,7 +130,7 @@ Qed. Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y. Proof. -intros x y H. pattern y; apply Plt_ind with x. +intros x y H. pattern y; apply Pos.lt_ind with x. rewrite phi_pos1_succ; apply (Rlt_succ_r sor). clear y H; intros y _ H. rewrite phi_pos1_succ. now apply (Rlt_lt_succ sor). assumption. @@ -150,9 +150,9 @@ apply -> (Ropp_lt_mono sor); apply clt_pos_morph. red. now rewrite Pos.compare_antisym. Qed. -Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y]. +Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y]. Proof. -unfold Zle_bool; intros x y H. +unfold Z.leb; intros x y H. case_eq (x ?= y)%Z; intro H1; rewrite H1 in H. le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1. le_less. now apply clt_morph. @@ -162,9 +162,9 @@ Qed. Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y]. Proof. intros x y H. unfold Zeq_bool in H. -case_eq (Zcompare x y); intro H1; rewrite H1 in *; (discriminate || clear H). +case_eq (Z.compare x y); intro H1; rewrite H1 in *; (discriminate || clear H). apply (Rlt_neq sor). now apply clt_morph. -fold (x > y)%Z in H1. rewrite Zgt_iff_lt in H1. +fold (x > y)%Z in H1. rewrite Z.gt_lt_iff in H1. apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph. Qed. |