Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Questions about two theorems

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Questions about two theorems


Chronological Thread 
  • From: "John Wiegley" <johnw AT newartisans.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Questions about two theorems
  • Date: Mon, 15 Sep 2014 16:50:17 +0100
  • Organization: New Artisans LLC

>>>>> Cedric Auger
>>>>> <sedrikov AT gmail.com>
>>>>> writes:

> You can then define a injection f which sends any (x:fin (S n)) such that
> (x≠hd) to some (y:fin n).

Thanks to you and Daniel, I am now much closer. However, I'm still having
difficulty with the above statement: what about the case where hd is not the
greatest element of fin (S n)? Then the fact that x <> hd doesn't help me,
since hd could be an element which *should* be in y, rather than x. It seems
like your proof assumes an ordered set from greatest to last, when the
original statement requires no ordering. Daniel did make reference to the
fact that having a sorting property could make things easier.

John



Archive powered by MHonArc 2.6.18.

Top of Page