diff options
Diffstat (limited to 'theories/ZArith/Zquot.v')
| -rw-r--r-- | theories/ZArith/Zquot.v | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index e93ebb1a..264109dc 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms. +Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms. Local Open Scope Z_scope. @@ -37,17 +37,17 @@ Notation Ndiv_Zquot := N2Z.inj_quot (only parsing). Notation Nmod_Zrem := N2Z.inj_rem (only parsing). Notation Z_quot_rem_eq := Z.quot_rem' (only parsing). Notation Zrem_lt := Z.rem_bound_abs (only parsing). -Notation Zquot_unique := Z.quot_unique (compat "8.6"). -Notation Zrem_unique := Z.rem_unique (compat "8.6"). -Notation Zrem_1_r := Z.rem_1_r (compat "8.6"). -Notation Zquot_1_r := Z.quot_1_r (compat "8.6"). -Notation Zrem_1_l := Z.rem_1_l (compat "8.6"). -Notation Zquot_1_l := Z.quot_1_l (compat "8.6"). -Notation Z_quot_same := Z.quot_same (compat "8.6"). +Notation Zquot_unique := Z.quot_unique (compat "8.7"). +Notation Zrem_unique := Z.rem_unique (compat "8.7"). +Notation Zrem_1_r := Z.rem_1_r (compat "8.7"). +Notation Zquot_1_r := Z.quot_1_r (compat "8.7"). +Notation Zrem_1_l := Z.rem_1_l (compat "8.7"). +Notation Zquot_1_l := Z.quot_1_l (compat "8.7"). +Notation Z_quot_same := Z.quot_same (compat "8.7"). Notation Z_quot_mult := Z.quot_mul (only parsing). -Notation Zquot_small := Z.quot_small (compat "8.6"). -Notation Zrem_small := Z.rem_small (compat "8.6"). -Notation Zquot2_quot := Zquot2_quot (compat "8.6"). +Notation Zquot_small := Z.quot_small (compat "8.7"). +Notation Zrem_small := Z.rem_small (compat "8.7"). +Notation Zquot2_quot := Zquot2_quot (compat "8.7"). (** Particular values taken for [a÷0] and [(Z.rem a 0)]. We avise to not rely on these arbitrary values. *) @@ -129,33 +129,33 @@ Qed. Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0. Proof. intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. @@ -171,12 +171,12 @@ Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r. Proof. unfold Remainder, Remainder_alt; intuition. - - romega with *. - - romega with *. - - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega. + - lia. + - lia. + - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia. - assert (0 <= Z.sgn r * Z.sgn a). { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } - destruct r; simpl Z.sgn in *; romega with *. + destruct r; simpl Z.sgn in *; lia. Qed. Theorem Zquot_mod_unique_full a b q r : @@ -185,7 +185,7 @@ Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. apply Zdiv_mod_unique with b; auto. apply Zrem_lt_pos; auto. - romega with *. + lia. rewrite <- H1; apply Z.quot_rem'. rewrite <- (Z.opp_involutive a). @@ -193,7 +193,7 @@ Proof. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. - romega with *. + lia. Qed. Theorem Zquot_unique_full a b q r : |