I think "Proof by cases" uses proof by contradiction. You're proving that given A -> C and !A -> C, then C, which requires the axiom A v !A, i.e. proof by contr

I think "Proof by cases" uses proof by contradiction. You're proving that given A -> C and !A -> C, then C, which requires the axiom A v !A, i.e. proof by contradiction. In your proof, you've proven k=0 -> X != 2, and k > 0 -> X !=2, but it doesn't follow that X != 2 without contradiction.