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