proposition: Lemma list_before_rev l x y : list_before (rev l) x y <-> list_before l y x.
proof: Proof. unfold list_before; rewrite nodup_rev; intuition; desf. - apply (f_equal (@rev _)) in H1. repeat first [rewrite rev_involutive in * | rewrite rev_app_distr in *; ins ]. desf; rewrite <- !app_assoc; ins; eauto. - repeat (rewrite rev_app_distr; ins). rewrite <- !app_assoc; ins; eauto. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic