Best practice simple task

[alex4482]

Hi.
I need to add an element to end of list, and i found snoc (l,x) in the docs.
But i actually need to prove that snoc returns a list that is bigger by exactly 1.
It seems obvious to me, and i would just write an assume(length x = length y + 1 ) but i dont think this is best practice.
Thought I should write a Lemma to prove it, but i wasnt sure how. Just return ( )?, or have to make induction like in tutorials?

[nikswamy]

You can use FStar.List.Tot.Properties. lemma_snoc_length

[alex4482]

i cant find it in docs. only lemma_unsnoc_length

[nikswamy]

https://github.com/FStarLang/FStar/blob/master/ulib/FStar.List.Tot.Properties.fst#L359

[klinvill]

As a side note, the docs are currently not comprehensive. I've found it easiest to just look at the relevant files under ulib when looking to see what lemmas and functions exist (and do).