Coq: proof of "lens is closed under composition"

I'm a functional programmer completely new to Coq. In fact, I've just finished Mike Naha's tutorial. Particularly, I'm interested in this language to formalize some laws related to optics. For example, I'd like to know how to encode that lens is closed under composition.

I started to deal with GetPut. The aforementioned tutorial doesn't cover records, but I think they're what I need to encode a lens. As far as I know, the composition method should be implemented as a Definition. Finally, I assume that my theorem needs to receive evidences of GetPut for the composing lenses, to prove that the same law holds for the resulting lens by means of an equality. Not very helpful, but this is my (incomplete and wrong) proof skeleton:

Record lens (S : Type) (A : Type) := mkLens {
  get : S -> A;
  put : S -> A -> S }.

Definition compose_ln (S A B : Type) (ln1: lens S A) (ln2 : lens A B) : lens S B :=
  {| get := fun (s : S) => get ln1 s;
     put := fun (s : S) (a : A) => put ln1 s (put ln2 (get ln1 s) a) |}.

Theorem closed_GetPut :
    (forall S A B : Type,
    (forall (s : S),
    (forall (ln1 : lens S A) (ln2 : lens A B),
    (exists GetPut_proof : ln1 (* ln1 holds GetPut? *)),
    (exists GetPut_proof : ln2 (* ln2 holds GetPut? *)),
    (put (compose_ln ln1 ln2) s (get (compose_ln ln1 ln2) s) = s)))).
Proof.
  (* ... *)
Qed.

Having said so:

Am I in the right path to write this proof? Is there any other way to better approach it?
Where can I find similar examples to be used as guiding examples?
Based on my FP background, what's the better material to keep on learning Coq? (I was thinking on Software Foundations by Benjamin C. Pierce.)

Thank you!

Solution

This looks roughly reasonable, but it needs some tidying.

First, you might as well remove the two "exists" quantifiers (change them into plain implications).

Second, the types of the two last assumptions should not be just "ln1" and "ln2" but something like "very_well_behaved ln1" and "very_well_behaved ln2". (And then the type of the final result can be "very_well_behaved (compose ln2 ln2)".