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.