Basic facts on Z

Arithmetic over nat

Section narith.

Lemma le_trans : forall l k n : N, k <= l -> l <= n -> k <= n.

Lemma minus_n_Sk : forall n k : N, k < n -> n - k = S (n - S k).

Lemma le_minus : forall n k : N, n - k <= n.

Lemma minus_n_minus_n_k : forall k n : N, k <= n -> k = n - (n - k).

End narith.

Arithmetic over Z

Section zarith.

Definition Zdec : forall a : Z, {a = 0%Z} + {a <> 0%Z}.
Defined.

Lemma unique_unit : forall u : Z, (forall a : Z, (a * u)%Z = a) -> u = 1%Z.

Lemma Zmult_zero_div : forall a b : Z, (a * b)%Z = 0%Z -> a = 0%Z \/ b = 0%Z.

Lemma Zmult_no_zero_div :
forall a b : Z, a <> 0%Z -> b <> 0%Z -> (a * b)%Z <> 0%Z.

Lemma Zmult_unit_oneforall :
forall u a : Z, a <> 0%Z -> (a * u)%Z = a -> forall b : Z, (b * u)%Z = b.

Lemma Zunit_eq_one : forall u a : Z, a <> 0%Z -> (a * u)%Z = a -> u = 1%Z.

Lemma Zmult_intro_lft :
forall a b c : Z, a <> 0%Z -> (a * b)%Z = (a * c)%Z -> b = c.

Lemma Zmult_intro_rht :
forall a b c : Z, a <> 0%Z -> (b * a)%Z = (c * a)%Z -> b = c.

Lemma succ_nat: forall (m:nat),Zpos (P_of_succ_nat m) = (Z_of_nat m + 1)%Z.

End zarith.

Facts on inequalities over Z

Section zineq.

Lemma Zgt_Zge: forall (n m:Z), (n>m)%Z -> (n>=m)%Z.

Lemma Zle_antisymm : forall a b : Z, (a >= b)%Z -> (b >= a)%Z -> a = b.

Definition Zlt_irref : forall a : Z, ~ (a < a)%Z := Zlt_irrefl.

Lemma Zgt_irref : forall a : Z, ~ (a > a)%Z.

Lemma Zlt_NEG_0 : forall p : positive, (Zneg p < 0)%Z.

Lemma Zgt_0_NEG : forall p : positive, (0 > Zneg p)%Z.

Lemma Zle_NEG_0 : forall p : positive, (Zneg p <= 0)%Z.

Lemma Zge_0_NEG : forall p : positive, (0 >= Zneg p)%Z.

Lemma Zle_NEG_1 : forall p : positive, (Zneg p <= -1)%Z.

Lemma Zge_1_NEG : forall p : positive, (-1 >= Zneg p)%Z.

Lemma Zlt_0_POS : forall p : positive, (0 < Zpos p)%Z.

Lemma Zgt_POS_0 : forall p : positive, (Zpos p > 0)%Z.

Lemma Zle_0_POS : forall p : positive, (0 <= Zpos p)%Z.

Lemma Zge_POS_0 : forall p : positive, (Zpos p >= 0)%Z.

Lemma Zle_1_POS : forall p : positive, (1 <= Zpos p)%Z.

Lemma Zge_POS_1 : forall p : positive, (Zpos p >= 1)%Z.

Lemma Zle_neg_pos : forall p q : positive, (Zneg p <= Zpos q)%Z.

Lemma ZPOS_neq_ZERO : forall p : positive, Zpos p <> 0%Z.

Lemma ZNEG_neq_ZERO : forall p : positive, Zneg p <> 0%Z.

Lemma Zge_gt_succ : forall a b : Z, (a >= b + 1)%Z -> (a > b)%Z.

Lemma Zge_gt_pred : forall a b : Z, (a - 1 >= b)%Z -> (a > b)%Z.

Lemma Zgt_ge_succ : forall a b : Z, (a + 1 > b)%Z -> (a >= b)%Z.

Lemma Zgt_ge_pred : forall a b : Z, (a > b - 1)%Z -> (a >= b)%Z.

Lemma Zlt_asymmetric : forall a b : Z, {(a < b)%Z} + {a = b} + {(a > b)%Z}.

Lemma Zle_neq_lt : forall a b : Z, (a <= b)%Z -> a <> b -> (a < b)%Z.

Lemma Zmult_pos_mon_le_lft :
forall a b c : Z, (a >= b)%Z -> (c >= 0)%Z -> (c * a >= c * b)%Z.

Lemma Zmult_pos_mon_le_rht :
forall a b c : Z, (a >= b)%Z -> (c >= 0)%Z -> (a * c >= b * c)%Z.

Lemma Zmult_pos_mon_lt_lft :
forall a b c : Z, (a > b)%Z -> (c > 0)%Z -> (c * a > c * b)%Z.

Lemma Zmult_pos_mon_lt_rht :
forall a b c : Z, (a > b)%Z -> (c > 0)%Z -> (a * c > b * c)%Z.

Lemma Zmult_pos_mon : forall a b : Z, (a * b > 0)%Z -> (a * b >= a)%Z.

Lemma Zdiv_pos_pos : forall a b : Z, (a * b > 0)%Z -> (a > 0)%Z -> (b > 0)%Z.

Lemma Zdiv_pos_nonneg :
forall a b : Z, (a * b > 0)%Z -> (a >= 0)%Z -> (b > 0)%Z.

Lemma Zdiv_pos_neg : forall a b : Z, (a * b > 0)%Z -> (a < 0)%Z -> (b < 0)%Z.

Lemma Zdiv_pos_nonpos :
forall a b : Z, (a * b > 0)%Z -> (a <= 0)%Z -> (b < 0)%Z.

Lemma Zdiv_neg_pos : forall a b : Z, (a * b < 0)%Z -> (a > 0)%Z -> (b < 0)%Z.

Lemma Zdiv_neg_nonneg :
forall a b : Z, (a * b < 0)%Z -> (a >= 0)%Z -> (b < 0)%Z.

Lemma Zdiv_neg_neg : forall a b : Z, (a * b < 0)%Z -> (a < 0)%Z -> (b > 0)%Z.

Lemma Zdiv_neg_nonpos :
forall a b : Z, (a * b < 0)%Z -> (a <= 0)%Z -> (b > 0)%Z.

Lemma Zcompat_lt_plus: forall (n m p:Z),(n < m)%Z-> (p+n < p+m)%Z.

Lemma lt_succ_Z_of_nat: forall (m:nat)( k n:Z),
(Z_of_nat (S m)<(k+n))%Z -> (Z_of_nat m <(k+n))%Z.

End zineq.

Facts on the absolute value-function over Z

Section zabs.

Lemma Zabs_idemp : forall a : Z, Zabs (Zabs a) = Zabs a.

Lemma Zabs_nonneg : forall (a : Z) (p : positive), Zabs a <> Zneg p.

Lemma Zabs_geq_zero : forall a : Z, (0 <= Zabs a)%Z.

Lemma Zabs_elim_nonneg : forall a : Z, (0 <= a)%Z -> Zabs a = a.

Lemma Zabs_zero : forall a : Z, Zabs a = 0%Z -> a = 0%Z.

Lemma Zabs_Zopp : forall a : Z, Zabs (- a) = Zabs a.

Lemma Zabs_geq : forall a : Z, (a <= Zabs a)%Z.

Lemma Zabs_Zopp_geq : forall a : Z, (- a <= Zabs a)%Z.

Lemma Zabs_Zminus_symm : forall a b : Z, Zabs (a - b) = Zabs (b - a).

Lemma Zabs_lt_pos : forall a b : Z, (Zabs a < b)%Z -> (0 < b)%Z.

Lemma Zabs_le_pos : forall a b : Z, (Zabs a <= b)%Z -> (0 <= b)%Z.

Lemma Zabs_lt_elim :
forall a b : Z, (a < b)%Z -> (- a < b)%Z -> (Zabs a < b)%Z.

Lemma Zabs_le_elim :
forall a b : Z, (a <= b)%Z -> (- a <= b)%Z -> (Zabs a <= b)%Z.

Lemma Zabs_mult_compat : forall a b : Z, (Zabs a * Zabs b)%Z = Zabs (a * b).

Let case_POS :
  forall p q r : positive,
  (Zpos q + Zneg p)%Z = Zpos r ->
  (Zabs (Zpos q + Zneg p) <= Zabs (Zpos q) + Zabs (Zneg p))%Z.
Defined.

Let case_NEG :
  forall p q r : positive,
  (Zpos q + Zneg p)%Z = Zneg r ->
  (Zabs (Zpos q + Zneg p) <= Zabs (Zpos q) + Zabs (Zneg p))%Z.

Defined.

Lemma Zabs_triangle : forall a b : Z, (Zabs (a + b) <= Zabs a + Zabs b)%Z.

Lemma Zabs_Zminus_triangle :
forall a b : Z, (Zabs (Zabs a - Zabs b) <= Zabs (a - b))%Z.

End zabs.

Facts on the sign-function over Z

Section zsign.

Lemma Zsgn_mult_compat : forall a b : Z, (Zsgn a * Zsgn b)%Z = Zsgn (a * b).

Lemma Zmult_sgn_abs : forall a : Z, (Zsgn a * Zabs a)%Z = a.

Lemma Zmult_sgn_eq_abs : forall a : Z, Zabs a = (Zsgn a * a)%Z.

Lemma Zsgn_plus_l : forall a b : Z, Zsgn a = Zsgn b -> Zsgn (a + b) = Zsgn a.

Lemma Zsgn_plus_r : forall a b : Z, Zsgn a = Zsgn b -> Zsgn (a + b) = Zsgn b.

Lemma Zsgn_opp : forall z : Z, Zsgn (- z) = (- Zsgn z)%Z.

Lemma Zsgn_ZERO : forall z : Z, Zsgn z = 0%Z -> z = 0%Z.

Lemma Zsgn_pos : forall z : Z, Zsgn z = 1%Z -> (z > 0)%Z.

Lemma Zsgn_neg : forall z : Z, Zsgn z = (-1)%Z -> (z < 0)%Z.

End zsign.