# Library Coq.omega.OmegaLemmas

Require Import ZArith_base.
Open Local Scope Z_scope.

Factorization lemmas

Theorem Zred_factor0 : forall n:Z, n = n * 1.

Theorem Zred_factor1 : forall n:Z, n + n = n * 2.

Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m).

Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m).

Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p).

Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m.

Theorem Zred_factor6 : forall n:Z, n = n + 0.

Other specific variants of theorems dedicated for the Omega tactic

Lemma new_var : forall x : Z, exists y : Z, x = y.

Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y.

Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y.

Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0.

Lemma OMEGA4 : forall x y z : Z, x > 0 -> y > x -> z * y + x <> 0.

Lemma OMEGA5 : forall x y z : Z, x = 0 -> y = 0 -> x + y * z = 0.

Lemma OMEGA6 : forall x y z : Z, 0 <= x -> y = 0 -> 0 <= x + y * z.

Lemma OMEGA7 :
forall x y z t : Z, z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t.

Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0.

Lemma OMEGA9 : forall x y z t : Z, y = 0 -> x = z -> y + (- x + z) * t = 0.

Lemma OMEGA10 :
forall v c1 c2 l1 l2 k1 k2 : Z,
(v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).

Lemma OMEGA11 :
forall v1 c1 l1 l2 k1 : Z,
(v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).

Lemma OMEGA12 :
forall v2 c2 l1 l2 k2 : Z,
l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).

Lemma OMEGA13 :
forall (v l1 l2 : Z) (x : positive),
v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2.

Lemma OMEGA14 :
forall (v l1 l2 : Z) (x : positive),
v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
Lemma OMEGA15 :
forall v c1 c2 l1 l2 k2 : Z,
v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).

Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k.

Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.

Lemma OMEGA18 : forall x y k : Z, x = y * k -> Zne x 0 -> Zne y 0.

Lemma OMEGA19 : forall x : Z, Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1.

Lemma OMEGA20 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.

Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop)
(H : P (y + x)) := eq_ind_r P H (Zplus_comm x y).

Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop)
(H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p).

Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop)
(H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p).

Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop)
(H : P (m + (n + p))) := eq_ind_r P H (Zplus_permute n m p).

Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2 : Z) (P : Z -> Prop)
(H : P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))) :=
eq_ind_r P H (OMEGA10 v c1 c2 l1 l2 k1 k2).

Definition fast_OMEGA11 (v1 c1 l1 l2 k1 : Z) (P : Z -> Prop)
(H : P (v1 * (c1 * k1) + (l1 * k1 + l2))) :=
eq_ind_r P H (OMEGA11 v1 c1 l1 l2 k1).
Definition fast_OMEGA12 (v2 c2 l1 l2 k2 : Z) (P : Z -> Prop)
(H : P (v2 * (c2 * k2) + (l1 + l2 * k2))) :=
eq_ind_r P H (OMEGA12 v2 c2 l1 l2 k2).

Definition fast_OMEGA15 (v c1 c2 l1 l2 k2 : Z) (P : Z -> Prop)
(H : P (v * (c1 + c2 * k2) + (l1 + l2 * k2))) :=
eq_ind_r P H (OMEGA15 v c1 c2 l1 l2 k2).
Definition fast_OMEGA16 (v c l k : Z) (P : Z -> Prop)
(H : P (v * (c * k) + l * k)) := eq_ind_r P H (OMEGA16 v c l k).

Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
(H : P (l1 + l2)) := eq_ind_r P H (OMEGA13 v l1 l2 x).

Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
(H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x).
Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop)
(H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x).

Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop)
(H : P (x * -1)) := eq_ind_r P H (Zopp_eq_mult_neg_1 x).

Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop)
(H : P (y * x)) := eq_ind_r P H (Zmult_comm x y).

Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop)
(H : P (- x + - y)) := eq_ind_r P H (Zopp_plus_distr x y).

Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) :=
eq_ind_r P H (Zopp_involutive x).

Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop)
(H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y).

Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop)
(H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p).
Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop)
(H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y).

Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop)
(H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p).

Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop)
(H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x).

Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop)
(H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor2 x y).

Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop)
(H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor3 x y).

Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop)
(H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z).

Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
(H : P y) := eq_ind_r P H (Zred_factor5 x y).

Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
(H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).