proposition: Theorem max_lt_iff : ∀ n m p, p < max n m ↔ p < n ∨ p < m.
proof: Proof. intros n m p. split; intros H. destruct p as [p| ]; [ idtac | inversion H ]. destruct n as [n| ]; [ idtac | left; constructor ]. destruct m as [m| ]; [ idtac | right; constructor ]. inversion_clear H; subst. apply Nat.max_lt_iff in H0. destruct H0; [ left | right ]; constructor; assumption. destruct p as [p| ]; [ idtac | destruct H; inversion H ]. destruct n as [n| ]; [ idtac | constructor ]. destruct m as [m| ]; [ idtac | constructor ]. constructor. apply Nat.max_lt_iff. destruct H as [H| H]; [ left | right ]; inversion H; assumption. Qed.
imports: Utf8 Compare_dec NPeano Misc