proposition: Lemma max_case_strong : forall n m (P:t -> Type), (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
proof: Proof. intros; apply max_case_strong; auto. congruence. Defined.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics