proposition: Lemma Rbar_min_case_strong (r1 r2 : Rbar) (P : Rbar -> Type) : (Rbar_le r1 r2 -> P r1) -> (Rbar_le r2 r1 -> P r2) -> P (Rbar_min r1 r2).
proof: Proof. case: r1 => [x | | ] //= ; case: r2 => [y | | ] //= Hx Hy ; (try by apply Hx) ; (try by apply Hy). by apply Rmin_case_strong. Qed.
imports: Coq(Reals ssreflect) Rcomplements