proposition: Lemma not_empty P n : O < count n P -> { i | i < n /\ P i = true }.
proof: Proof. intros CP. induction n. simpl in CP; impossible. simpl in CP. rem (P n) Pn EPn; destruct Pn. exists n; auto. destruct IHn as (i, Hi); dumb. exists i; dumb. Defined.
imports: ZArith Lia MyNat