diff options
Diffstat (limited to 'theories/ZArith/Zquot.v')
| -rw-r--r-- | theories/ZArith/Zquot.v | 351 |
1 files changed, 134 insertions, 217 deletions
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index 9a95669f..c02f0ae6 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.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 *) @@ -11,51 +11,95 @@ Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms. Local Open Scope Z_scope. (** This file provides results about the Round-Toward-Zero Euclidean - division [Zquotrem], whose projections are [Zquot] and [Zrem]. - Definition of this division can be found in file [BinIntDef]. + division [Z.quotrem], whose projections are [Z.quot] (noted ÷) + and [Z.rem]. - This division and the one defined in Zdiv agree only on positive - numbers. Otherwise, Zdiv performs Round-Toward-Bottom (a.k.a Floor). + This division and [Z.div] agree only on positive numbers. + Otherwise, [Z.div] performs Round-Toward-Bottom (a.k.a Floor). - The current approach is compatible with the division of usual + This [Z.quot] is compatible with the division of usual programming languages such as Ocaml. In addition, it has nicer properties with respect to opposite and other usual operations. + + The definition of this division is now in file [BinIntDef], + while most of the results about here are now in the main module + [BinInt.Z], thanks to the generic "Numbers" layer. Remain here: + + - some compatibility notation for old names. + + - some extra results with less preconditions (in particular + exploiting the arbitrary value of division by 0). *) -(** * Relation between division on N and on Z. *) +Notation Ndiv_Zquot := N2Z.inj_quot (compat "8.3"). +Notation Nmod_Zrem := N2Z.inj_rem (compat "8.3"). +Notation Z_quot_rem_eq := Z.quot_rem' (compat "8.3"). +Notation Zrem_lt := Z.rem_bound_abs (compat "8.3"). +Notation Zquot_unique := Z.quot_unique (compat "8.3"). +Notation Zrem_unique := Z.rem_unique (compat "8.3"). +Notation Zrem_1_r := Z.rem_1_r (compat "8.3"). +Notation Zquot_1_r := Z.quot_1_r (compat "8.3"). +Notation Zrem_1_l := Z.rem_1_l (compat "8.3"). +Notation Zquot_1_l := Z.quot_1_l (compat "8.3"). +Notation Z_quot_same := Z.quot_same (compat "8.3"). +Notation Z_quot_mult := Z.quot_mul (compat "8.3"). +Notation Zquot_small := Z.quot_small (compat "8.3"). +Notation Zrem_small := Z.rem_small (compat "8.3"). +Notation Zquot2_quot := Zquot2_quot (compat "8.3"). + +(** Particular values taken for [a÷0] and [(Z.rem a 0)]. + We avise to not rely on these arbitrary values. *) + +Lemma Zquot_0_r a : a ÷ 0 = 0. +Proof. now destruct a. Qed. + +Lemma Zrem_0_r a : Z.rem a 0 = a. +Proof. now destruct a. Qed. + +(** The following results are expressed without the [b<>0] condition + whenever possible. *) + +Lemma Zrem_0_l a : Z.rem 0 a = 0. +Proof. now destruct a. Qed. + +Lemma Zquot_0_l a : 0÷a = 0. +Proof. now destruct a. Qed. + +Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r + : zarith. -Lemma Ndiv_Zquot : forall a b:N, - Z_of_N (a/b) = (Z_of_N a ÷ Z_of_N b). -Proof. - intros. - destruct a; destruct b; simpl; auto. - unfold N.div, Z.quot; simpl. destruct N.pos_div_eucl; auto. -Qed. +Ltac zero_or_not a := + destruct (Z.eq_decidable a 0) as [->|?]; + [rewrite ?Zquot_0_l, ?Zrem_0_l, ?Zquot_0_r, ?Zrem_0_r; + auto with zarith|]. -Lemma Nmod_Zrem : forall a b:N, - Z.of_N (a mod b) = Z.rem (Z.of_N a) (Z.of_N b). -Proof. - intros. - destruct a; destruct b; simpl; auto. - unfold N.modulo, Z.rem; simpl; destruct N.pos_div_eucl; auto. -Qed. +Lemma Z_rem_same a : Z.rem a a = 0. +Proof. zero_or_not a. now apply Z.rem_same. Qed. -(** * Characterization of this euclidean division. *) +Lemma Z_rem_mult a b : Z.rem (a*b) b = 0. +Proof. zero_or_not b. now apply Z.rem_mul. Qed. -(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] - has been chosen to be [a], so this equation holds even for [b=0]. -*) +(** * Division and Opposite *) -Notation Z_quot_rem_eq := Z.quot_rem' (only parsing). +(* The precise equalities that are invalid with "historic" Zdiv. *) -(** Then, the inequalities constraining the remainder: - The remainder is bounded by the divisor, in term of absolute values *) +Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b). +Proof. zero_or_not b. now apply Z.quot_opp_l. Qed. -Theorem Zrem_lt : forall a b:Z, b<>0 -> - Z.abs (Z.rem a b) < Z.abs b. -Proof. - apply Z.rem_bound_abs. -Qed. +Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b). +Proof. zero_or_not b. now apply Z.quot_opp_r. Qed. + +Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b). +Proof. zero_or_not b. now apply Z.rem_opp_l. Qed. + +Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b. +Proof. zero_or_not b. now apply Z.rem_opp_r. Qed. + +Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b. +Proof. zero_or_not b. now apply Z.quot_opp_opp. Qed. + +Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b). +Proof. zero_or_not b. now apply Z.rem_opp_opp. Qed. (** The sign of the remainder is the one of [a]. Due to the possible nullity of [a], a general result is to be stated in the following form: @@ -63,41 +107,33 @@ Qed. Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a. Proof. - destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; - simpl; destruct n0; simpl; auto with zarith. + zero_or_not b. + - apply Z.square_nonneg. + - zero_or_not (Z.rem a b). + rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg. Qed. (** This can also be said in a simplier way: *) Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a. Proof. - rewrite <-Z.sgn_nonneg, Z.sgn_mul; apply Zrem_sgn. + zero_or_not b. + - apply Z.square_nonneg. + - now apply Z.rem_sign_mul. Qed. -(** Reformulation of [Zquot_lt] and [Zrem_sgn] in 2 - then 4 particular cases. *) +(** Reformulation of [Z.rem_bound_abs] in 2 then 4 particular cases. *) Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b. Proof. - intros. - assert (0 <= Z.rem a b). - generalize (Zrem_sgn a b). - destruct (Zle_lt_or_eq 0 a H). - rewrite <- Zsgn_pos in H1; rewrite H1. romega with *. - subst a; simpl; auto. - generalize (Zrem_lt a b H0); romega with *. + intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b); + romega with *. Qed. Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0. Proof. - intros. - assert (Z.rem a b <= 0). - generalize (Zrem_sgn a b). - destruct (Zle_lt_or_eq a 0 H). - rewrite <- Zsgn_neg in H1; rewrite H1; romega with *. - subst a; simpl; auto. - generalize (Zrem_lt a b H0); romega with *. + intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b); + romega with *. Qed. Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b. @@ -120,45 +156,6 @@ Proof. intros; generalize (Zrem_lt_neg a b); romega with *. Qed. -(** * Division and Opposite *) - -(* The precise equalities that are invalid with "historic" Zdiv. *) - -Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b. -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b. -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. (** * Unicity results *) @@ -172,170 +169,93 @@ 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 <-(Zmult_opp_opp). - apply Zmult_le_0_compat; romega. - assert (0 <= Z.sgn r * Z.sgn a) by (rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto). - destruct r; simpl Z.sgn in *; romega with *. + - romega with *. + - romega with *. + - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega. + - assert (0 <= Z.sgn r * Z.sgn a). + { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } + destruct r; simpl Z.sgn in *; romega with *. Qed. -Theorem Zquot_mod_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> q = a÷b /\ r = Z.rem a b. +Theorem Zquot_mod_unique_full a b q r : + Remainder a b r -> a = b*q + r -> q = a÷b /\ r = Z.rem a b. Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. apply Zdiv_mod_unique with b; auto. apply Zrem_lt_pos; auto. romega with *. - rewrite <- H1; apply Z_quot_rem_eq. + rewrite <- H1; apply Z.quot_rem'. - rewrite <- (Zopp_involutive a). + rewrite <- (Z.opp_involutive a). rewrite Zquot_opp_l, Zrem_opp_l. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). - rewrite <-Z_quot_rem_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1. + rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. romega with *. Qed. -Theorem Zquot_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> q = a÷b. +Theorem Zquot_unique_full a b q r : + Remainder a b r -> a = b*q + r -> q = a÷b. Proof. intros; destruct (Zquot_mod_unique_full a b q r); auto. Qed. -Theorem Zquot_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> - a = b*q + r -> q = a÷b. -Proof. exact Z.quot_unique. Qed. - -Theorem Zrem_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> r = Z.rem a b. +Theorem Zrem_unique_full a b q r : + Remainder a b r -> a = b*q + r -> r = Z.rem a b. Proof. intros; destruct (Zquot_mod_unique_full a b q r); auto. Qed. -Theorem Zrem_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> - a = b*q + r -> r = Z.rem a b. -Proof. exact Z.rem_unique. Qed. - -(** * Basic values of divisions and modulo. *) - -Lemma Zrem_0_l: forall a, Z.rem 0 a = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zrem_0_r: forall a, Z.rem a 0 = a. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zquot_0_l: forall a, 0÷a = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zquot_0_r: forall a, a÷0 = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zrem_1_r: forall a, Z.rem a 1 = 0. -Proof. exact Z.rem_1_r. Qed. - -Lemma Zquot_1_r: forall a, a÷1 = a. -Proof. exact Z.quot_1_r. Qed. - -Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r - : zarith. - -Lemma Zquot_1_l: forall a, 1 < a -> 1÷a = 0. -Proof. exact Z.quot_1_l. Qed. - -Lemma Zrem_1_l: forall a, 1 < a -> Z.rem 1 a = 1. -Proof. exact Z.rem_1_l. Qed. - -Lemma Z_quot_same : forall a:Z, a<>0 -> a÷a = 1. -Proof. exact Z.quot_same. Qed. - -Ltac zero_or_not a := - destruct (Z.eq_dec a 0); - [subst; rewrite ?Zrem_0_l, ?Zquot_0_l, ?Zrem_0_r, ?Zquot_0_r; - auto with zarith|]. - -Lemma Z_rem_same : forall a, Z.rem a a = 0. -Proof. intros. zero_or_not a. apply Z.rem_same; auto. Qed. - -Lemma Z_rem_mult : forall a b, Z.rem (a*b) b = 0. -Proof. intros. zero_or_not b. apply Z.rem_mul; auto. Qed. - -Lemma Z_quot_mult : forall a b:Z, b <> 0 -> (a*b)÷b = a. -Proof. exact Z.quot_mul. Qed. - (** * Order results about Zrem and Zquot *) (* Division of positive numbers is positive. *) -Lemma Z_quot_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a÷b. +Lemma Z_quot_pos a b : 0 <= a -> 0 <= b -> 0 <= a÷b. Proof. intros. zero_or_not b. apply Z.quot_pos; auto with zarith. Qed. (** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) -Lemma Z_quot_lt : forall a b:Z, 0 < a -> 2 <= b -> a÷b < a. +Lemma Z_quot_lt a b : 0 < a -> 2 <= b -> a÷b < a. Proof. intros. apply Z.quot_lt; auto with zarith. Qed. -(** A division of a small number by a bigger one yields zero. *) +(** [<=] is compatible with a positive division. *) -Theorem Zquot_small: forall a b, 0 <= a < b -> a÷b = 0. -Proof. exact Z.quot_small. Qed. - -(** Same situation, in term of modulo: *) - -Theorem Zrem_small: forall a n, 0 <= a < n -> Z.rem a n = a. -Proof. exact Z.rem_small. Qed. - -(** [Zge] is compatible with a positive division. *) - -Lemma Z_quot_monotone : forall a b c, 0<=c -> a<=b -> a÷c <= b÷c. +Lemma Z_quot_monotone a b c : 0<=c -> a<=b -> a÷c <= b÷c. Proof. intros. zero_or_not c. apply Z.quot_le_mono; auto with zarith. Qed. -(** With our choice of division, rounding of (a÷b) is always done toward zero: *) +(** With our choice of division, rounding of (a÷b) is always done toward 0: *) -Lemma Z_mult_quot_le : forall a b:Z, 0 <= a -> 0 <= b*(a÷b) <= a. +Lemma Z_mult_quot_le a b : 0 <= a -> 0 <= b*(a÷b) <= a. Proof. intros. zero_or_not b. apply Z.mul_quot_le; auto with zarith. Qed. -Lemma Z_mult_quot_ge : forall a b:Z, a <= 0 -> a <= b*(a÷b) <= 0. +Lemma Z_mult_quot_ge a b : a <= 0 -> a <= b*(a÷b) <= 0. Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed. (** The previous inequalities between [b*(a÷b)] and [a] are exact iff the modulo is zero. *) -Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> Z.rem a b = 0. +Lemma Z_quot_exact_full a b : a = b*(a÷b) <-> Z.rem a b = 0. Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. (** A modulo cannot grow beyond its starting point. *) -Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> Z.rem a b <= a. +Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. (** Some additionnal inequalities about Zdiv. *) Theorem Zquot_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a÷b <= q. -Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_upper_bound. Qed. +Proof. intros a b q; rewrite Z.mul_comm; apply Z.quot_le_upper_bound. Qed. Theorem Zquot_lt_upper_bound: forall a b q, 0 <= a -> 0 < b -> a < q*b -> a÷b < q. -Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_lt_upper_bound. Qed. +Proof. intros a b q; rewrite Z.mul_comm; apply Z.quot_lt_upper_bound. Qed. Theorem Zquot_le_lower_bound: forall a b q, 0 < b -> q*b <= a -> q <= a÷b. -Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_lower_bound. Qed. +Proof. intros a b q; rewrite Z.mul_comm; apply Z.quot_le_lower_bound. Qed. Theorem Zquot_sgn: forall a b, 0 <= Z.sgn (a÷b) * Z.sgn a * Z.sgn b. @@ -374,22 +294,22 @@ Proof. intros. zero_or_not b. apply Z.quot_mul_cancel_r; auto. Qed. Lemma Zquot_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)÷(c*b) = a÷b. Proof. - intros. rewrite (Zmult_comm c b). zero_or_not b. - rewrite (Zmult_comm b c). apply Z.quot_mul_cancel_l; auto. + intros. rewrite (Z.mul_comm c b). zero_or_not b. + rewrite (Z.mul_comm b c). apply Z.quot_mul_cancel_l; auto. Qed. Lemma Zmult_rem_distr_l: forall a b c, Z.rem (c*a) (c*b) = c * (Z.rem a b). Proof. - intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b. - rewrite (Zmult_comm b c). apply Z.mul_rem_distr_l; auto. + intros. zero_or_not c. rewrite (Z.mul_comm c b). zero_or_not b. + rewrite (Z.mul_comm b c). apply Z.mul_rem_distr_l; auto. Qed. Lemma Zmult_rem_distr_r: forall a b c, Z.rem (a*c) (b*c) = (Z.rem a b) * c. Proof. - intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c. - rewrite (Zmult_comm c b). apply Z.mul_rem_distr_r; auto. + intros. zero_or_not b. rewrite (Z.mul_comm b c). zero_or_not c. + rewrite (Z.mul_comm c b). apply Z.mul_rem_distr_r; auto. Qed. (** Operations modulo. *) @@ -424,7 +344,7 @@ Lemma Zplus_rem_idemp_r: forall a b n, Z.rem (b + Z.rem a n) n = Z.rem (b + a) n. Proof. intros. zero_or_not n. apply Z.add_rem_idemp_r; auto. - rewrite Zmult_comm; auto. + rewrite Z.mul_comm; auto. Qed. Lemma Zmult_rem_idemp_l: forall a b n, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. @@ -437,8 +357,8 @@ Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_r; auto. Qed. Lemma Zquot_Zquot : forall a b c, (a÷b)÷c = a÷(b*c). Proof. - intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c. - rewrite Zmult_comm. apply Z.quot_quot; auto. + intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. + rewrite Z.mul_comm. apply Z.quot_quot; auto. Qed. (** A last inequality: *) @@ -468,28 +388,26 @@ Proof. right. destruct p; simpl; split; now auto with zarith. Qed. -Notation Zquot2_quot := Zquot2_quot (only parsing). - Lemma Zrem_odd : forall a, Z.rem a 2 = if Z.odd a then Z.sgn a else 0. Proof. intros. symmetry. - apply Zrem_unique_full with (Zquot2 a). + apply Zrem_unique_full with (Z.quot2 a). apply Zquot2_odd_remainder. apply Zquot2_odd_eqn. Qed. Lemma Zrem_even : forall a, Z.rem a 2 = if Z.even a then 0 else Z.sgn a. Proof. - intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Zeven_bool. + intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Z.even. Qed. -Lemma Zeven_rem : forall a, Z.even a = Zeq_bool (Z.rem a 2) 0. +Lemma Zeven_rem : forall a, Z.even a = Z.eqb (Z.rem a 2) 0. Proof. intros a. rewrite Zrem_even. destruct a as [ |p|p]; trivial; now destruct p. Qed. -Lemma Zodd_rem : forall a, Z.odd a = negb (Zeq_bool (Z.rem a 2) 0). +Lemma Zodd_rem : forall a, Z.odd a = negb (Z.eqb (Z.rem a 2) 0). Proof. intros a. rewrite Zrem_odd. destruct a as [ |p|p]; trivial; now destruct p. @@ -505,18 +423,17 @@ Proof. intros. apply Zdiv_mod_unique with b. apply Zrem_lt_pos; auto with zarith. - rewrite Zabs_eq; auto with *; apply Z_mod_lt; auto with *. + rewrite Z.abs_eq; auto with *; apply Z_mod_lt; auto with *. rewrite <- Z_div_mod_eq; auto with *. - symmetry; apply Z_quot_rem_eq; auto with *. + symmetry; apply Z.quot_rem; auto with *. Qed. Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> a÷b = a/b. Proof. - intros a b Ha Hb. - destruct (Zle_lt_or_eq _ _ Hb). - generalize (Zquotrem_Zdiv_eucl_pos a b Ha H); intuition. - subst; rewrite Zquot_0_r, Zdiv_0_r; reflexivity. + intros a b Ha Hb. Z.le_elim Hb. + - generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb); intuition. + - subst; now rewrite Zquot_0_r, Zdiv_0_r. Qed. Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b -> |