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