Library Coq.Numbers.Integer.Abstract.ZAdd
Require Export ZBase.
Module ZAddPropFunct (
Import ZAxiomsMod :
ZAxiomsSig).
Module Export ZBasePropMod :=
ZBasePropFunct ZAxiomsMod.
Open Local Scope IntScope.
Theorem Zadd_wd :
forall n1 n2 :
Z,
n1 ==
n2 ->
forall m1 m2 :
Z,
m1 ==
m2 ->
n1 +
m1 ==
n2 +
m2.
Theorem Zadd_0_l :
forall n :
Z, 0 +
n ==
n.
Theorem Zadd_succ_l :
forall n m :
Z, (
S n) +
m ==
S (
n +
m).
Theorem Zsub_0_r :
forall n :
Z,
n - 0 ==
n.
Theorem Zsub_succ_r :
forall n m :
Z,
n - (
S m) ==
P (
n -
m).
Theorem Zopp_0 : - 0 == 0.
Theorem Zopp_succ :
forall n :
Z, - (
S n) ==
P (-
n).
Theorem Zadd_0_r :
forall n :
Z,
n + 0 ==
n.
Theorem Zadd_succ_r :
forall n m :
Z,
n +
S m ==
S (
n +
m).
Theorem Zadd_comm :
forall n m :
Z,
n +
m ==
m +
n.
Theorem Zadd_assoc :
forall n m p :
Z,
n + (
m +
p) == (
n +
m) +
p.
Theorem Zadd_shuffle1 :
forall n m p q :
Z, (
n +
m) + (
p +
q) == (
n +
p) + (
m +
q).
Theorem Zadd_shuffle2 :
forall n m p q :
Z, (
n +
m) + (
p +
q) == (
n +
q) + (
m +
p).
Theorem Zadd_1_l :
forall n :
Z, 1 +
n ==
S n.
Theorem Zadd_1_r :
forall n :
Z,
n + 1 ==
S n.
Theorem Zadd_cancel_l :
forall n m p :
Z,
p +
n ==
p +
m <->
n ==
m.
Theorem Zadd_cancel_r :
forall n m p :
Z,
n +
p ==
m +
p <->
n ==
m.
Theorem Zadd_pred_l :
forall n m :
Z,
P n +
m ==
P (
n +
m).
Theorem Zadd_pred_r :
forall n m :
Z,
n +
P m ==
P (
n +
m).
Theorem Zadd_opp_r :
forall n m :
Z,
n + (-
m) ==
n -
m.
Theorem Zsub_0_l :
forall n :
Z, 0 -
n == -
n.
Theorem Zsub_succ_l :
forall n m :
Z,
S n -
m ==
S (
n -
m).
Theorem Zsub_pred_l :
forall n m :
Z,
P n -
m ==
P (
n -
m).
Theorem Zsub_pred_r :
forall n m :
Z,
n - (
P m) ==
S (
n -
m).
Theorem Zopp_pred :
forall n :
Z, - (
P n) ==
S (-
n).
Theorem Zsub_diag :
forall n :
Z,
n -
n == 0.
Theorem Zadd_opp_diag_l :
forall n :
Z, -
n +
n == 0.
Theorem Zadd_opp_diag_r :
forall n :
Z,
n + (-
n) == 0.
Theorem Zadd_opp_l :
forall n m :
Z, -
m +
n ==
n -
m.
Theorem Zadd_sub_assoc :
forall n m p :
Z,
n + (
m -
p) == (
n +
m) -
p.
Theorem Zopp_involutive :
forall n :
Z, - (-
n) ==
n.
Theorem Zopp_add_distr :
forall n m :
Z, - (
n +
m) == -
n + (-
m).
Theorem Zopp_sub_distr :
forall n m :
Z, - (
n -
m) == -
n +
m.
Theorem Zopp_inj :
forall n m :
Z, -
n == -
m ->
n ==
m.
Theorem Zopp_inj_wd :
forall n m :
Z, -
n == -
m <->
n ==
m.
Theorem Zeq_opp_l :
forall n m :
Z, -
n ==
m <->
n == -
m.
Theorem Zeq_opp_r :
forall n m :
Z,
n == -
m <-> -
n ==
m.
Theorem Zsub_add_distr :
forall n m p :
Z,
n - (
m +
p) == (
n -
m) -
p.
Theorem Zsub_sub_distr :
forall n m p :
Z,
n - (
m -
p) == (
n -
m) +
p.
Theorem sub_opp_l :
forall n m :
Z, -
n -
m == -
m -
n.
Theorem Zsub_opp_r :
forall n m :
Z,
n - (-
m) ==
n +
m.
Theorem Zadd_sub_swap :
forall n m p :
Z,
n +
m -
p ==
n -
p +
m.
Theorem Zsub_cancel_l :
forall n m p :
Z,
n -
m ==
n -
p <->
m ==
p.
Theorem Zsub_cancel_r :
forall n m p :
Z,
n -
p ==
m -
p <->
n ==
m.
Theorem Zadd_move_l :
forall n m p :
Z,
n +
m ==
p <->
m ==
p -
n.
Theorem Zadd_move_r :
forall n m p :
Z,
n +
m ==
p <->
n ==
p -
m.
Theorem Zsub_move_l :
forall n m p :
Z,
n -
m ==
p <-> -
m ==
p -
n.
Theorem Zsub_move_r :
forall n m p :
Z,
n -
m ==
p <->
n ==
p +
m.
Theorem Zadd_move_0_l :
forall n m :
Z,
n +
m == 0 <->
m == -
n.
Theorem Zadd_move_0_r :
forall n m :
Z,
n +
m == 0 <->
n == -
m.
Theorem Zsub_move_0_l :
forall n m :
Z,
n -
m == 0 <-> -
m == -
n.
Theorem Zsub_move_0_r :
forall n m :
Z,
n -
m == 0 <->
n ==
m.
Theorem Zadd_simpl_l :
forall n m :
Z,
n +
m -
n ==
m.
Theorem Zadd_simpl_r :
forall n m :
Z,
n +
m -
m ==
n.
Theorem Zsub_simpl_l :
forall n m :
Z, -
n -
m +
n == -
m.
Theorem Zsub_simpl_r :
forall n m :
Z,
n -
m +
m ==
n.
Theorem Zadd_add_simpl_l_l :
forall n m p :
Z, (
n +
m) - (
n +
p) ==
m -
p.
Theorem Zadd_add_simpl_l_r :
forall n m p :
Z, (
n +
m) - (
p +
n) ==
m -
p.
Theorem Zadd_add_simpl_r_l :
forall n m p :
Z, (
n +
m) - (
m +
p) ==
n -
p.
Theorem Zadd_add_simpl_r_r :
forall n m p :
Z, (
n +
m) - (
p +
m) ==
n -
p.
Theorem Zsub_add_simpl_r_l :
forall n m p :
Z, (
n -
m) + (
m +
p) ==
n +
p.
Theorem Zsub_add_simpl_r_r :
forall n m p :
Z, (
n -
m) + (
p +
m) ==
n +
p.
End ZAddPropFunct.