I have the following definition of divisibility by 3.
Inductive div3 : nat -> Prop :=
| div0 : div3 0
| divS : forall n : nat, div3_2 n -> div3 (S n)
with div3_2 : nat -> Prop :=
| div2 : div3_2 2
| div2S : forall n : nat, div3_1 n -> div3_2 (S n)
with div3_1 : nat -> Prop :=
| div1 : div3_1 1
| div1S : forall n : nat, div3 n -> div3_1 (S n).
How can I go about proving the following lemma?
Lemma practice : forall n : nat, div3 n -> exists m, n = 3 * m.