proposition: Lemma Rbar_min_case (x y : Rbar) (P : Rbar -> Type) : P x -> P y -> P (Rbar_min x y).
proof: Proof. case: x => [x | | ] //= ; case: y => [y | | ] //=. by apply Rmin_case. Qed.
imports: Coq(Reals ssreflect) Rcomplements