get field from Record Types in Coq

Question

I am new to Coq. I have a record type and one definition:

Record t : Type := T {
  width           : nat;
}.

Definition indent shift f :=
  match f with
  | T w => T
    (w + shift)
  end.

I want to proof a trivial lemma:

Lemma lemma :
  forall (a:t) n, width a <= width (indent n a).

after unfolding indent subgoal becomes:

(width a <= width match a with
                   | {| width := w |} => {| width := w + n |}
                   end)

How to simplify term?

Answer 1

destruct a. simpl.

After that induction.

Answer 2

Use a different definition and simpl will do the work:

Definition indent shift f := T (f.(width) + shift).

Answer 3

When you see a term with match a with ... end in it, you can simplify it by doing destruct a. Also if you need to get rid of let a := b in ... If you need to remember what a was, do destruct a eqn:Ha.