proposition: Theorem sup_swap I J (f: I -> J -> X) I' J': sup (fun i => sup (fun j => f i j) J') I' ≡ sup (fun j => sup (fun i => f i j) I') J'.
proof: Proof. induction I'; simpl. apply antisym. apply leq_bx. apply leq_supx; trivial. now rewrite IHI', supcup. Qed.
imports: lset lattice ordinal