induction.v

Inductive gorgeous : nat -> Prop :=
  g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).
Fixpoint gorgeous_ind_max (P: forall n, gorgeous n -> Prop) (f : P 0 g_0)
         (f0 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (3+m) (g_plus3 m e)) 
         (f1 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (5+m) (g_plus5 m e)) 
         (n : nat) (e: gorgeous n) : P n e :=
  match e in (gorgeous n0) return (P n0 e) with
    | g_0 => f
    | g_plus3 n0 g0 => f0 n0 g0 (gorgeous_ind_max P f f0 f1 n0 g0)
    | g_plus5 n0 g0 => f1 n0 g0 (gorgeous_ind_max P f f0 f1 n0 g0)
  end.
Check gorgeous_ind_max.
(*
gorgeous_ind_max
     : forall P : forall n : nat, gorgeous n -> Prop,
       P 0 g_0 ->
       (forall (m : nat) (e : gorgeous m), P m e -> P (3 + m) (g_plus3 m e)) ->
       (forall (m : nat) (e : gorgeous m), P m e -> P (5 + m) (g_plus5 m e)) ->
       forall (n : nat) (e : gorgeous n), P n e
*)
Check gorgeous_ind.
(*
gorgeous_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, gorgeous n -> P n -> P (3 + n)) ->
       (forall n : nat, gorgeous n -> P n -> P (5 + n)) ->
       forall n : nat, gorgeous n -> P n
*)