Library Arith_ext

Require Import Omega.
Require Import ssreflect ssrbool.
Export Arith.


Lemma le_plus_minus_r2 : forall m n, m <= n -> n - m + m = n.

Lemma plus_minus_assoc : forall b a c, c <= b -> a + b - c = a + (b - c).

Lemma le_minus_trans : forall a b c, a <= c -> a - b <= c.












Lemma minus_lt_compat : forall a n m, m < n -> n <= a -> a - n < a - m.


Lemma scale_le : forall a, 1 <= a -> forall b, b <= a * b.

Lemma scale_lt : forall a, 1 < a -> forall b, 1 <= b -> b < a * b.

Lemma le_neq_lt : forall n m, n <= m -> n <> m -> n < m.

Lemma my_mult_lt_compat_l: forall a b c, a * c < b * c -> c >= 1 -> a < b.

Lemma mult_lt_compat_0 : forall a b, O <> a -> O <> b -> 0 < a * b.

Lemma mult_reg_r : forall n m p, p <> O -> n * p = m * p -> n = m.


Lemma inv_lt : forall k a b, 0 < k -> 0 < b -> a * k < b * k -> a < b.

Lemma constant_zero : forall n k a b, a < b -> a + n * b = k * b -> a = 0.

Fixpoint nat_gt (n m : nat) {struct n} : bool :=
  match n with
    | 0 => false
    | S n' => match m with
                | 0 => true
                | S m' => nat_gt n' m'
              end
  end.

Fixpoint power (b : nat) (e : nat) : nat :=
  match e with
    | O => 1
    | S e' => b * power b e'
  end.

Lemma power_S : forall k n, power k (S n) = k * power k n.

Lemma power_plus : forall n, power 2 n + power 2 n = power 2 (S n).

Lemma power_is_exp : forall n m, power 2 (n + m) = power 2 n * power 2 m.

Lemma le_1_power : forall n, 1 <= power 2 n.

Fixpoint isum n := if n is S n' then (isum n') + S n' else O.

Lemma isum_prop' : forall a, isum (S a) = isum a + (S a).



Lemma minus_Sn_1 : forall n, S n - 1 = n.

Lemma minus_Sn_n : forall n, S n - n = 1.

Lemma minus_minus : forall n m p, n - m - p = n - (m + p).