proposition: Lemma f_sup_eq {X Y: ops} (f: X -> Y): (f bot = bot) -> (forall x y, f (x ⊔ y) = f x ⊔ f y) -> forall I J (g: I -> X), f (sup g J) = \sup_(i\in J) f (g i).
proof: Proof. intros Hbot Hcup I J g. induction J. apply Hbot. simpl. rewrite Hcup. congruence. Qed.
imports: lset lattice ordinal