1 subgoal
l : nat
H : 0 < l
______________________________________(1/1)
match l with
| 0 => true :: nil
| S _ => g_one l ++ false :: nil
end = g_one l ++ false :: nil

this seems trivially true, but I can’t figure out how to get Coq to see that - any suggestions?

A match will simplify when the head starts with a constructor, so you need a way to rewrite l into S l' for some l', which suggests to use the following intermediate step:

assert (exists l', l = S l').

Another idea (to combine with the above or not) is to use inversion (maybe twice) because < is defined using an inductive type.

You can also search for a lemma about < (lt) and 0 to solve that intermediate step:

SearchAbout lt 0.

One result that seems particularly relevant is

S_pred_pos: forall n : nat, 0 < n -> n = S (Nat.pred n)