proposition: Lemma reorderK po a b (NIN: ~ po b a) (IN: po a b) : reorder (reorder po a b) b a ≡ po.
proof: Proof. Proof using. unfold reorder; split; red; ins; desf; intuition. destruct (classic (x = a)); desf; destruct (classic (y = b)); desf; intuition; left; intuition; desf. Qed.
imports: HahnBase HahnList HahnRelationsBasic