# Help with strong induction

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.

• We're not a proof-completion service. Please moderate your questions because you will saturate the collective willingness to help by posting random questions in which you do not even indicate what you've tried and what the problem is. May 16 at 13:08

As div3 is defined using a mutual inductive definition with div3_1 and div3_2. The stronger statement you may try to prove is

Lemma practice :
(forall n : nat, div3 n -> exists m, n = 3 * m) /\
(forall n : nat, div3_1 n -> exists m, n = 3 * m + 1) /\
(forall n : nat, div3_2 n -> exists m, n = 3 * m + 2).


A possible solution is to prove a slightly modified version of practice by a single induction on n, using inversion tactics.

Lemma practice n :
(div3 n -> exists m, n = 3 * m) /\
(div3_1 n -> exists m, n = S (3 * m)) /\
(div3_2 n -> exists m, n = 2 + 3 * m ).
Proof.
induction n.
- repeat split; now exists 0.
-  destruct IHn as [H0 [H1 H2]]; repeat split.
+ inversion_clear 1.
destruct (H2 H3) as [x Hx]; exists (S x); subst; ring.
+ inversion  1.
* subst n; exists 0; ring.
* subst n0; destruct (H0 H4) as [x Hx]; exists x; now subst.
+ inversion 1.
* subst n ; now exists 0.
* destruct (H1 H4) as [x Hx];  subst ; exists x; ring.
Qed.


For a better understanding, you may replace the use of inversion with diy "inversion lemmas" .

Lemma div3_inv n : div3 n -> n = 0 \/ exists p, n = S p /\ div3_2 p.
Proof.
destruct 1 as [|n Hn].
- now left.
- right; exists n; auto.
Qed.

(* ... *)