I am getting error

$"[$Focus$]$ Wrong bullet $-$: Current bullet $-$ is not finished."

for the line $"-$ intros contra. inversion Hdiv; subst. apply IHn; auto."

And cannot use "auto" in the code

Help my fix this code:

Require Import Arith.

$(*$ Define the accessiblity predicate $*)$

Inductive acc : nat $->$ Prop :$=$

$|$ acc$\_$k : forall k$,($forall y$,$ y $<$ k $->$ acc y$)->$ acc k$.$

$(*$ Define a proof of well$-$foundedness of $<$ relation $*)$

Theorem lt$\_$wf : forall n$,$ acc n$.$

Proof.

induction n$.$

$-$ apply acc$\_$k$.$ intros y H$.$ inversion H$.$

$-$ apply acc$\_$k$.$ intros y Hlt$.$ apply IHn.

Qed.

$(*$ Define a function acc$\_$then$\_$Px which converts a proof of accessibility to a proof of predicate P $*)$

Definition acc$\_$then$\_$Px : forall $($P : nat $->$ Prop$)($n : nat$),$

$($forall x$,($forall y$,$ y $<$ x $->$ P y$)->$ P x$)->$ acc n $->$ P n$.$

Proof.

refine $($fun P n f acc $=>$

acc$\_$ind $\_\_$ acc

$($fun k f$\text{'}=>$ f k $($fun y Hy $=>$ acc$\_$then$\_$Px P y $($fun $\_=>$ f$\text{'})($f$\text{'}$ y Hy$)))$

acc$).$

Defined.

$(*$ Define a strong natural induction principle $*)$

Definition strong$\_$nat$\_$ind : forall $($P : nat $->$ Prop$),$

$($forall x$,($forall y$,$ y $<$ x $->$ P y$)->$ P x$)->$ forall x$,$ P x$.$

Proof.

refine $($fun P f x $=>$ acc$\_$then$\_$Px P x f $($lt$\_$wf x$)).$

Defined.

$(*$ Define the div$4$ and rem$2$ predicates $*)$

Inductive div$4$ : nat $->$ Prop :$=$

$|$ div$4\_0$ : div$40$

$|$ div$4\_$S : forall n$,$ rem$2$ n $->$ div$4($S $($S n$))$

with rem$2$ : nat $->$ Prop :$=$

$|$ rem$2\_$S : forall n$,$ div$4$ n $->$ rem$2($S $($S n$)).$

$(*$ Lemma prob$4$: div$4$ n $->$ ~rem$2$ n $*)$

Lemma prob$4$ : forall n$,$ div$4$ n $->$ ~rem$2$ n$.$

Proof.

intros n Hdiv.

induction n using strong$\_$nat$\_$ind.

$-$ intros contra. inversion Hdiv.

$-$ intros contra. inversion Hdiv; subst. apply IHn; auto.

Qed.