proposition: Lemma min_case_strong n m (P:O.t -> Type) : (forall x y, x == y -> P x -> P y) -> (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
proof: Proof. intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. - assert (n<=m) by (rewrite le_lteq; auto). apply (Compat n), Hl; auto. symmetry; apply min_l; auto. - assert (n<=m) by (rewrite le_lteq; auto). apply (Compat n), Hl; auto. symmetry; apply min_l; auto. - assert (m<=n) by (rewrite le_lteq; auto). apply (Compat m), Hr; auto. symmetry; apply min_r; auto. Defined.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics