Library aux

Require Export LibTactics LibReflect LibRelation LibNat LibVar LibList LibListSorted LibFset Morphisms LibListExt LibFsetExt Utf8.

Fixpoint lt_dec (m n : nat) :=
match m, n with
| O, Ofalse
| O, S _true
| S _, Ofalse
| S , S lt_dec
end.

Instance lt_decidable : (m n : nat), Decidable (m<n).
Proof. intros. applys¬ decidable_make (lt_dec m n).
gen n. induction m; intros; destruct n; simpl.
symmetry. apply¬ isTrue_false. nat_math.
symmetry. apply¬ isTrue_true. nat_math.
symmetry. apply¬ isTrue_false. nat_math.
asserts_rewrite ((S m < S n) = (m < n)).
extens. iff; nat_math.
auto.
Qed.

Lemma min_same: n, (min n n) = n.
Proof.
induction n; simpls¬.
Qed.

Hint Resolve min_same.

Definition max (m n : nat) := ifb (m < n) then n else m.

Lemma max0 : m n, max m n = 0 → m = 0 n = 0.
Proof.
introv H. unfolds in H; cases_if~; nat_math.
Qed.

Lemma max0neutrall : m, max 0 m = m.
Proof.
introv. unfolds. cases_if; nat_math.
Qed.

Lemma max0neutralr : m, max m 0 = m.
Proof.
introv. unfolds. cases_if; nat_math.
Qed.

Lemma maxcomm : m n, max m n = max n m.
Proof.
introv. unfolds; cases_if; cases_if~; nat_math.
Qed.

Lemma maxassoc : m n p, max m (max n p) = max (max m n) p.
Proof.
introv. unfolds; repeat cases_if~; nat_math.
Qed.