proposition: Lemma first_non_zero (f : nat -> nat) n : f 0 = 0 -> f n <> 0 -> exists i, i < n /\ (forall k, k <= i -> f k = 0) /\ f (i+1) <> 0.
proof: Proof. intros H0 H1. destruct (@minimize (fun i => f i <> 0)) as (i & H2 & H3). + intro; destruct (eq_nat_dec (f x) 0); lia. + exists n; auto. + assert (i <> 0) as Hi by (intro; subst; destruct H2; auto). exists (i-1); split; [ | split ]. * destruct (le_lt_dec i n) as [ | H4 ]; try lia. apply H3 in H4; destruct H4; auto. * intros k Hk; generalize (H3 k); intros; lia. * replace (i-1+1) with i by lia; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)