The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 11/30/2015 12:38 PM, Volker Stolz wrote:
> Require Import Ensembles.
> Require Import Lt.
>
> Fixpoint ss n : Ensemble nat :=
>    match n with
>    | 0 => Singleton _ 0
>    | S m => Add _ (ss m) (S m)
>    end.
>
> Lemma succNotInSS: forall n x, x > n -> ~ In _ (ss n) x.
> Proof.
> Admitted.
>
> E.g., ss 1 := {0,1}, and show that no x>1 in (ss 1). It seems a proof by
> induction is going nowhere, since I always end up having to prove that
> an even larger value is also not in there.
>
> Could anyone please hint me at what I am missing?

If you rewrite your goal as

forall n x, ~ In _ (ss n) (S (n + x)).

an induction on n makes you use the induction principle for (S x)

--
Laurent