Ssreflect Users Discussion List

[Yves Bertot <>]

The statement expected for fconnect_step should be:

Lemma fconnect_step (T : finType) (f : T -> T) (x y : T) :
  fconnect f x y -> (f x == y) || (fconnect f (f x) y).


On 09/07/2018 08:07 AM, Yves Bertot wrote:
> Hello,
>
> I would like to show the following theorems.
>
> Lemma fconnect_step (T : finType) (f : T -> T) (x y : T) :
>   fconnect f x y -> f x == y || fconnect (f x) y.
>
> Lemma order_step (T : finType) (f : T -> T) (x y : T) :
>   fingraph.order f x = fingraph.order f (f x) /\
>     iter (fingraph.order f x) f x = x \/
>   order f x = (order f (f x)).+1.
>
> Lemma findex_step (T : finType) (f : T -> T) (x y : T) :
>   fconnect f x y ->
>   y != x -> findex f x y = (findex f (f x) y).+1.
>
> Each one is expected to be useful for the next one.  But the 
> interfaces provided for connect, findex, and order are very slim and I 
> am wondering whether I am using the right level of abstraction.  Does 
> anybody have an opinion on this?
>
> Yves