no goals
n : ℕ
⊢ descFactorial n 0 = 0 ↔ n < 0
simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k
n k : ℕ
⊢ descFactorial n (succ k) = 0 ↔ n < succ k
rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, lt_succ_iff,
  tsub_eq_zero_iff_le, lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
no goals
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k
exact fun h _ => h