proposition: Lemma list_before_snoc_other a l x y (NEQ: a <> y) : list_before (l ++ a :: nil) x y <-> list_before l x y /\ ~ In a l.
proof: Proof. rewrite list_before_snoc; intuition. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic