theorem Nat.doubleFactorial_pos {n : ℕ} : 0 < Nat.doubleFactorial n

theorem Nat.doubleFactorial_le_factorial {n : ℕ} : Nat.doubleFactorial n ≤ Nat.factorial n