Fixpoint fun1 (l : list nat) :=
 match l with
| nil => 1
| b::nil=> b
| b::t => gcd b (fun1 t)
end.

Lemma g_function: forall (l : list nat),
 l <> nil -> list_max l = 0-> fun1 l=0.
I want to apply Nat.gcd_diag to prove above lemma. I have proved following lemma also(Lemma list_max_0 l: list_max l = 0 ->
forall a, nth a l 0 = 0.Admitted.)

Require Import List Lia.

Fixpoint fun1 (l : list nat) :=
 match l with
| nil => 1
| b::nil=> b
| b::t => Nat.gcd b (fun1 t)
end.

Theorem aux a b: max a b = 0 -> a = 0 /\ b = 0.
Proof.
  intros. destruct a, b.
  + auto.
  + simpl in *. lia.
  + rewrite Max.max_comm in H. simpl in *. lia.
  + simpl in *. lia.
Qed.

Lemma g_function: forall (l : list nat), l <> nil -> list_max l = 0 -> fun1 l = 0.
Proof.
  intros. induction l.
  + congruence.
  + clear H. simpl in *. pose proof (aux _ _ H0). destruct H.
    rewrite H. destruct l.
    - reflexivity.
    - rewrite IHl.
      * simpl in *. reflexivity.
      * congruence.
      * auto.
Qed.