Я пытаюсь доказать eqb_neq:
Theorem eqb_neq : forall x y : nat,
x =? y = false <-> x <> y.
Это мой текущий статус доказательства: 
Во время доказательства я достиг последний шаг, на котором мне просто нужно доказать дополнительную теорему о помощнике:
Theorem eqb_false_helper : forall n m : nat,
n <> m -> S n <> S m.
Я пробовал несколько стратегий, но теперь я даже не уверен, что можно доказать эту теорему о помощнике.
Я не уверен, как доказать базовый случай с помощью индукции: 
Что еще я могу попробовать? Какие-нибудь советы по поводу eqb_neq или теоремы о помощнике?
Спасибо