proposition: Lemma sup_spec f J x: sup f J ≦ x <-> forall i, In i J -> f i ≦ x.
proof: Proof. induction J; simpl. split. tauto. intro. lattice. rewrite cup_spec, IHJ. clear IHJ. intuition. now subst. Qed.
imports: lset lattice ordinal