proposition: Lemma P_sup {X: ops} {P: X -> Prop} I J (f: I -> X): P bot -> (forall x y, P x -> P y -> P (x ⊔ y)) -> (forall i, In i J -> P (f i)) -> P (sup f J).
proof: Proof. intros Hbot Hcup. induction J; intro H; simpl. apply Hbot. apply Hcup. apply H; now left. apply IHJ. intros. apply H. now right. Qed.
imports: lset lattice ordinal