I would prove forall n1, n1 = Succ n1 <-> False
instead, and put it in an autorewrite database.
Require Import Coq.Setoids.Setoid.
Lemma L1 : forall P1, (P1 <-> P1) <-> True.
Proof. tauto. Qed.
Hint Rewrite L1 : LogHints.
Lemma L2 : forall (S1 : Set) (e1 : S1), e1 = e1 <-> True.
Proof. tauto. Qed.
Hint Rewrite L2 : LogHints.
Lemma L3 : forall n1, O = S n1 <-> False.
Proof.
intros. split.
intros H1. inversion H1.
tauto.
Qed.
Lemma L4 : forall n1, S n1 = O <-> False.
Proof.
intros. split.
intros H1. inversion H1.
tauto.
Qed.
Lemma L5 : forall n1 n2, S n1 = S n2 <-> n1 = n2.
Proof.
intros. split.
intros H1. inversion H1 as [H2]. tauto.
intros H1. rewrite H1. tauto.
Qed.
Hint Rewrite L3 L4 L5 : NatHints.
Lemma L6 : forall n1, n1 = S n1 <-> False.
Proof.
induction n1 as [| n1 H1];
autorewrite with LogHints NatHints;
tauto.
Qed.
Lemma L7 : forall n1, S n1 = n1 <-> False.
Proof.
induction n1 as [| n1 H1];
autorewrite with LogHints NatHints;
tauto.
Qed.
Hint Rewrite L6 L7 : NatHints.