# Library rt.util.nat

Require Import rt.util.tactics rt.util.ssromega.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.

Section NatLemmas.

Lemma addnb (b1 b2 : bool) : (b1 + b2) != 0 = b1 || b2.
Proof.
by destruct b1,b2;
Qed.

Lemma subh1 :
m n p,
m n
m - n + p = m + p - n.
Proof. by ins; ssromega. Qed.

Lemma subh2 :
m1 m2 n1 n2,
m1 m2
n1 n2
(m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
Proof. by ins; ssromega. Qed.

Lemma subh3 :
m n p,
m + p n
n p
m n - p.
Proof.
ins. rewrite <- leq_add2r with (p := p).
Qed.

Lemma subh4:
m n p,
m n
p n
(m == n - p) = (p == n - m).
Proof.
intros; apply/eqP.
destruct (p == n - m) eqn:EQ.
by move: EQ ⇒ /eqP EQ; rewrite EQ subKn.
by apply negbT in EQ; unfold not; intro BUG;
rewrite BUG subKn ?eq_refl in EQ.
Qed.

m n p,
m n
(m - n = p m = p + n).
Proof.
by split; ins; ssromega.
Qed.

m n p,
m n
(p = m - n p + n = m).
Proof.
by split; ins; ssromega.
Qed.

Lemma ltSnm : n m, n.+1 < m n < m.
Proof.
by ins; apply ltn_trans with (n := n.+1); [by apply ltnSn |by ins].
Qed.

Lemma min_lt_same :
x y z,
minn x z < minn y z x < y.
Proof.
unfold minn; ins; desf.
{
apply negbT in Heq0; rewrite -ltnNge in Heq0.
by apply leq_trans with (n := z).
}
{
apply negbT in Heq; rewrite -ltnNge in Heq.
by apply (ltn_trans H) in Heq0; rewrite ltnn in Heq0.
}
by rewrite ltnn in H.
Qed.

a b c,
a c
b c
a + (b - c ) = a - c + b.
Proof.
intros× AgeC BgeC.
induction b;induction c;intros;try ssromega.
Qed.

Lemma ltn_subLR:
a b c,
a - c < b
a < b + c.
Proof.
intros× AC. ssromega.
Qed.

End NatLemmas.