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