proposition: Lemma in_prefix_of_nat_iff a n : In a (prefix_of_nat n) <-> exists i, i <= n /\ r^? a (f i) /\ s a.
proof: Proof. unfold clos_refl; induction n; ins; in_simp; repeat (rewrite ?in_app_iff, ?in_prefixes; ins; in_simp). intuition; desf; eauto; try (destruct i; ins; desf; eauto; lia). rewrite IHn; clear IHn; intuition; desf; try solve [exists i; splits; auto]; eauto. all: destruct (eqP i (S n)); [desf|assert (i <= n) by lia]; eauto 8. all: classical_right; splits; ins; eauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt