proposition: Lemma findP_spec A (cond : A -> Prop) (l : list A) n (IN: In n l) (COND: cond n) d : cond (nth (findP cond l) l d) /\ forall j, j < findP cond l -> ~ cond (nth j l d).
proof: Proof. induction l; ins; desf; splits; ins; desf; try lia; intuition. eauto using lt_S_n. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt