Library Lambda.TPOSR.MaxLemmas


Require
 Export
 Coq.Arith.Max.

Require
 Import
 Omega.







Definition
 max3 n
 m
 p
 := max n
 (max m
 p
).

Definition
 max4 n
 m
 p
 q
 := max n
 (max3 m
 p
 q
).

Definition
 max5 n
 m
 p
 q
 r
 := max n
 (max4 m
 p
 q
 r
).




Lemma
 max_lt_l : ∀ m
 n
, m
 < S (max m
 n
).




Lemma
 max_lt_r : ∀ m
 n
, n
 < S (max m
 n
).




Hint
 Resolve
 max_lt_l max_lt_r : arith
.




Lemma
 max3_lt_1 : ∀ m
 n
 p
, m
 < S (max3 m
 n
 p
).




Lemma
 max_n_0_n : ∀ m
, max m
 0 = m
.




Lemma
 max3_commut_1 : ∀ n
 m
 p
, max3 n
 m
 p
 = max3 m
 p
 n
.




Lemma
 max3_commut_2 : ∀ n
 m
 p
, max3 n
 m
 p
 = max3 p
 m
 n
.




Lemma
 max3_lt_2 : ∀ m
 n
 p
, n
 < S (max3 m
 n
 p
).




Lemma
 max3_lt_3 : ∀ m
 n
 p
, p
 < S (max3 m
 n
 p
).




Lemma
 max4_commut_1 : ∀ n
 m
 p
 q
, max4 n
 m
 p
 q
 = max4 m
 p
 q
 n
.




Lemma
 max4_commut_2 : ∀ n
 m
 p
 q
, max4 n
 m
 p
 q
 = max4 p
 q
 n
 m
.




Lemma
 max4_commut_3 : ∀ n
 m
 p
 q
, max4 n
 m
 p
 q
 = max4 q
 n
 m
 p
.




Lemma
 max4_lt_1 : ∀ m
 n
 p
 q
, m
 < S (max4 m
 n
 p
 q
).




Lemma
 max4_lt_2 : ∀ m
 n
 p
 q
, n
 < S (max4 m
 n
 p
 q
).




Lemma
 max4_lt_3 : ∀ m
 n
 p
 q
, p
 < S (max4 m
 n
 p
 q
).




Lemma
 max4_lt_4 : ∀ m
 n
 p
 q
, q
 < S (max4 m
 n
 p
 q
).




Lemma
 max_commut_2 : ∀ m
 n
 p
, max m
 (max n
 p
) = max n
 (max m
 p
).




Lemma
 max5_commut : ∀ n
 m
 p
 q
 r
, max5 n
 m
 p
 q
 r
 = max5 m
 p
 q
 r
 n
.




Lemma
 max5_commut_2 : ∀ n
 m
 p
 q
 r
, max5 n
 m
 p
 q
 r
 = max5 p
 q
 r
 n
 m
.




Lemma
 max5_commut_3 : ∀ n
 m
 p
 q
 r
, max5 n
 m
 p
 q
 r
 = max5 q
 r
 n
 m
 p
.




Lemma
 max5_commut_4 : ∀ n
 m
 p
 q
 r
, max5 n
 m
 p
 q
 r
 = max5 r
 n
 m
 p
 q
.




Lemma
 max5_lt_1 : ∀ m
 n
 p
 q
 r
, m
 < S (max5 m
 n
 p
 q
 r
).




Lemma
 max5_lt_2 : ∀ m
 n
 p
 q
 r
, n
 < S (max5 m
 n
 p
 q
 r
).




Lemma
 max5_lt_3 : ∀ m
 n
 p
 q
 r
, p
 < S (max5 m
 n
 p
 q
 r
).




Lemma
 max5_lt_4 : ∀ m
 n
 p
 q
 r
, q
 < S (max5 m
 n
 p
 q
 r
).




Lemma
 max5_lt_5 : ∀ m
 n
 p
 q
 r
, r
 < S (max5 m
 n
 p
 q
 r
).




Hint
 Resolve
 max3_lt_1 max3_lt_2 max3_lt_3 : arith
.

Hint
 Resolve
 max4_lt_1 max4_lt_2 max4_lt_3 max4_lt_4 : arith
.

Hint
 Resolve
 max5_lt_1 max5_lt_2 max5_lt_3 max5_lt_4 max5_lt_5 : arith
.