The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le vendredi 13 mai 2011 à 02:51 +0000, frank maltman a écrit :

>   IHf : fin_nat f < fin_bound f
>   ============================
>    S
>      ((fix fin_nat (b0 : nat) (f0 : fin b0) {struct f0} : nat :=
>          match f0 with
>          | FZ _ => 0
>          | FS b1 f' => S (fin_nat b1 f')
>          end) b f) < S b
> 
> I'm left scratching my head, unfortunately. I'm not sure what I need
> to be able to solve this.

If not for the leading S constructors in both sides, your goal would be
convertible to the induction hypothesis (since fin_bound f is b). So
just remove them with lemma lt_n_S and then apply the hypothesis.

Best regards,

Guillaume