Library hydras.Prelude.More_Arith

From Coq Require Import Arith Lia .
Import Nat.

Section Arith_lemmas.


Lemma nat_double_or_s_double :
  ∀ n, {∃ p, n = double p} + {∃ p, n = S (double p)}.

Lemma div2_double_is_id :∀ n : nat, div2 (double n) = n.

Lemma double_S (n:nat) : double (S n) = S (S (double n)).

Lemma double_plus (x y: nat): double (x + y)= double x + double y.

Lemma double_inj :
  ∀ (m n : nat), double m = double n → m = n.

Lemma double_is_even :
  ∀ n : nat, Nat.Even (double n).

Lemma not_double_is_s_double :
  ∀ (m n : nat), S (double m) ≠ double n.

Lemma div2_of_Even n: Nat.Even n → double (div2 n) = n.

Lemma even_prod :
  ∀ p q, Nat.Even ((p + q + 1) × (p + q)).

Lemma plus_2 :
  ∀ n, S (S n) = n + 2.

Lemma div2_incr :
  ∀ n m, n ≤ m → div2 n ≤ div2 m.

Lemma div2_even_plus :
  ∀ n m, Even n → div2 n + m = div2 (n + (double m)).

Lemma mult_lt_lt :
  ∀ p p' k, p × k < p' × k → p < p'.

Lemma minus_semi_assoc :
  ∀ a b c, b > c → a + (b - c) = (a + b) - c.

Lemma div_not_qlt :
  ∀ (a b : nat) (q q' r r' : nat),
    a = q × b + r → a = q' × b + r' → b > r → b > r' → ¬ q < q'.

Lemma div_eucl_unique :
  ∀ (a b : nat) (q q' r r' : nat),
    a = q × b + r → a = q' × b + r' → b > r → b > r' → q = q' ∧ r = r'.

Lemma max_le_plus (n p: nat) : Nat.max n p ≤ n + p.

Lemma max_le_regR : ∀ n p q, p ≤ q → max p n ≤ max q n.

Lemma max_le_regL : ∀ n p q, p ≤ q → max n p ≤ max n q.

Lemma lt_lt_Sn : ∀ a b c, a < b → b < S c → a < c.

End Arith_lemmas.

Notation power := Nat.pow (only parsing).

Lemma power_of_1 : ∀ p, power 1 p = 1.

Goal ∀ a b, 0 < power (S a) b.

Lemma pred_of_power : ∀ b e, pred (power (S b) (S e)) =
                                  (power (S b) e)*b +
                                  pred (power (S b) e).



Lemma get_predecessor : ∀ (n:nat), 0 < n → {p:nat | n = S p}.

Ltac pred_exhib H name :=
  match type of H
       with O < ?n ⇒
         case (get_predecessor H); intro name; intro
  end.


Lemma Euc1 : ∀ b q q' r r', 0 < b →
                                  q×b + r = q'×b + r' →
                                  r < b → r' < b → q = q'.