proposition: Lemma min_case_strong_r n m (P : nat -> Type) : (n <= m -> P n) -> (m < n -> P m) -> P (min n m).
proof: Proof. destruct (Compare_dec.le_lt_dec n m); first [ rewrite Nat.min_r by omega | rewrite Nat.min_l by omega ]; auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith