Library Z_misc
Require Import ZArith.
Require Import Znumtheory.
Require Import misc.
Property Zmin_right:
forall n m : Z,
(n >= m)%Z -> Zmin n m = m.
Proof.
intros n m n_ge_m.
elim (Zmin_spec n m); intuition.
Qed.
Property Zmin_left:
forall n m : Z,
(n <= m)%Z -> Zmin n m = n.
Proof.
intros n m n_ge_m.
elim (Zmin_spec n m); intuition.
Qed.
Property Zmax_le_compat_l:
forall n m p: Z, n <= m -> Zmax p n <= Zmax p m.
Proof.
intros n m p H_n_le_m.
elim (Zmax_spec p n).
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp H_max.
rewrite H_max.
apply Zle_max_l.
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp H_max.
rewrite H_max.
elim (Zmax_spec p m).
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp' H_max'.
absurd (p < n); auto.
apply Zle_not_lt.
apply (Zle_trans n m p); auto with zarith.
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp' H_max'.
rewrite H_max'.
assumption.
Qed.
Property Zmin_le_compat_l:
forall n m p: Z, n <= m -> Zmin p n <= Zmin p m.
Proof.
intros n m p H_n_le_m.
elim (Zmin_spec p n).
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp H_min.
rewrite H_min.
elim (Zmin_spec p m).
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp' H_min'.
rewrite H_min'.
apply Zle_refl.
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp' H_max'.
absurd (p > m); auto.
apply Zle_not_gt.
apply (Zle_trans p n m); auto with zarith.
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp H_min.
rewrite H_min.
elim (Zmin_spec p m).
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp' H_min'.
rewrite H_min'.
auto with zarith.
intro H_tmp; elim H_tmp; clear H_tmp.
intros H_cmp' H_max'.
rewrite H_max'.
assumption.
Qed.
Property Zabs_le_impl_between:
forall n m: Z,
Zabs n <= Zabs m -> - Zabs m <= n <= Zabs m.
Proof.
intros n m H_le.
split.
elim (Zabs_dec n); elim (Zabs_dec m).
intros H_m H_n.
apply Zle_left_rev.
rewrite Zopp_involutive.
rewrite Zplus_comm.
rewrite <- (Zopp_involutive n).
apply Zle_left.
rewrite H_n.
apply (Zle_trans (- Zabs n) 0 (Zabs m)); auto with zarith.
apply Zle_left_rev.
rewrite Zopp_involutive.
auto with zarith.
intros H_m H_n.
rewrite H_n.
apply (Zle_trans (- Zabs m) 0 (Zabs n)); auto with zarith.
apply Zle_left_rev.
rewrite Zopp_involutive.
auto with zarith.
intros H_m H_n.
rewrite H_n.
apply Zle_left_rev.
rewrite Zopp_involutive.
rewrite Zplus_comm.
apply Zle_left.
assumption.
intros H_m H_n.
rewrite H_n.
apply Zle_left_rev.
rewrite Zopp_involutive.
rewrite Zplus_comm.
apply Zle_left.
assumption.
elim (Zabs_dec n).
intros H_n.
rewrite H_n.
assumption.
intros H_n.
rewrite H_n.
apply (Zle_trans (- Zabs n) 0 (Zabs m)); auto with zarith.
apply Zle_left_rev.
rewrite Zopp_involutive.
auto with zarith.
Qed.
Lemma Zdiv_le_denom :
forall a b c, c >= 0 -> 0 < a <= b -> c / a >= c / b.
Proof.
intros a b c Hc [Ha Hb].
apply Zle_ge; apply Zdiv_le_lower_bound; auto with zarith.
rewrite Zmult_comm.
rewrite (Z_div_mod_eq c b) at 2; auto with zarith.
apply Zle_trans with (b * (c / b)).
apply Zmult_le_compat_r; auto.
apply Zdiv_le_lower_bound; auto with zarith.
elim (Z_mod_lt c b); auto with zarith.
Qed.
Corollary Zdiv_ge_denom :
forall a b c, c > 0 -> a >= b -> b > 0 -> c / a <= c / b.
Proof.
intros.
apply Zge_le.
apply Zdiv_le_denom; try split; auto with zarith.
Qed.
Lemma Zgcd_gt_0_l : forall a b, a > 0 -> Zgcd a b > 0.
Proof.
intros a b.
assert (H := Zgcd_is_pos a b).
destruct (Zle_lt_or_eq _ _ H); auto with zarith.
symmetry in H0; set (Zgcd_inv_0_l _ _ H0); auto with zarith.
Qed.
Lemma Zgcd_gt_0_r:
forall a b: Z,
b > 0 -> 0 < Zgcd a b.
Proof.
intros a b.
assert (H := Zgcd_is_pos a b).
destruct (Zle_lt_or_eq _ _ H); auto with zarith.
symmetry in H0; set (Zgcd_inv_0_r _ _ H0); auto with zarith.
Qed.
Property Zlt_impl_Zle:
forall x y: Z,
(x < y + Z_of_nat 1%nat)%Z -> (x <= y)%Z.
Proof.
intros.
apply Zle_left_rev.
replace (y + - x)%Z with ((y + 1) + -1 + - x)%Z; try omega.
apply Zlt_left.
auto.
Qed.
Property Zle_impl_Zlt:
forall x y: Z,
(x <= y)%Z -> (x < y + 1)%Z.
Proof.
intros.
apply (Zle_lt_trans x y (y + 1)%Z); auto with zarith.
Qed.
Property Zgt_impl_Zge:
forall (x: nat) (y: Z),
(Z_of_nat x + Z_of_nat 1%nat > y )%Z -> (Z_of_nat x >= y)%Z.
Proof.
intros x y H_cmp.
apply Zle_ge.
apply Zgt_lt in H_cmp.
apply Zlt_impl_Zle.
assumption.
Qed.