proposition: Lemma list_before_nth l i j d : NoDup l -> i < j < length l -> list_before l (nth i l d) (nth j l d).
proof: Proof. unfold list_before; split; ins; desc. eapply nth_split with (d := d) in H1; desf. eapply nth_split with (d := d) in H0; desf. rewrite H0 in H1 at 1; rewrite <- app_assoc in H1; ins. do 3 eexists. rewrite H1 at 1; f_equal; f_equal. rewrite H1, nth_app, Nat.sub_diag; desf. edestruct Nat.lt_irrefl; eauto. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic