proposition: Lemma inc_punctured_downward_subset : forall a x u: E, inc u (punctured_downward_subset a x) = (inc u (U a) & leq a u x & u <> x).
proof: Proof. ir. ap iff_eq; ir. ufi punctured_downward_subset H; Ztac. uh H1; ee; am. uh H1; ee; am. uf punctured_downward_subset; ap Z_inc. ee; am. uhg; xd. Qed.
imports: Arith order