Mod3.v

Inductive Mod3' : nat -> Prop :=
| zero' : forall n k, n = 3 * k     -> Mod3' n
| one'  : forall n k, n = 3 * k + 1 -> Mod3' n
| two'  : forall n k, n = 3 * k + 2 -> Mod3' n
.


Lemma nat_mod3' : forall n, Mod3' n.
Proof.
  induction n as [| n1 IHn ].
  (* 0 *)
    apply (zero' 0 0). reflexivity.

  (* n1 *)
    destruct IHn as [ n k HM0 | n k HM1 | n k HM2 ].
    apply (one' (S n) k).
    rewrite <- HM0. rewrite plus_comm.
    reflexivity.

    apply (two' (S n) k).
    rewrite -> HM1.
    rewrite (plus_comm (3 * k) 1). rewrite (plus_comm (3 * k) 2).
    reflexivity.

    apply (zero' (S n) (S k)).
    rewrite -> HM2.

    rewrite plus_comm.
    simpl.

    rewrite -> plus_0_r.

    rewrite <- plus_Snm_nSm.
    rewrite <- plus_Snm_nSm.

    simpl. rewrite <- plus_Snm_nSm.
    reflexivity.
Qed.


Definition mod3 n r : Prop := exists k, n = 3 * k + r.

Inductive Mod3 : nat -> Prop :=
| zero : forall n, mod3 n 0 -> Mod3 n
| one  : forall n, mod3 n 1 -> Mod3 n
| two  : forall n, mod3 n 2 -> Mod3 n
.