theorem exists_eq_card_filter_of_card_le_one {α : Type u_1} {p : α → Prop} [DecidablePred p] (A : Finset α) (h : (Finset.filter p A).card ≤ 1) : (if ∃ a ∈ A, p a then 1 else 0) = (Finset.filter p A).card

theorem min_sq (a : ℚ) (b : ℚ) (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : min a b ^ 2 = min (a ^ 2) (b ^ 2)

theorem half_le_floor_of_one_le (a : ℝ) (h : 1 ≤ a) : a / 2 ≤ ↑⌊a⌋₊