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