proposition: Lemma sup_leq' J J' (f f': I -> X): J ≦J' -> (forall i, In i J -> f i ≦ f' i) -> sup f J ≦ sup f' J'.
proof: Proof. induction J; intros HJ Hf. apply leq_bx. simpl. apply leq_cupx. rewrite Hf. apply leq_xsup. apply HJ. now left. now left. apply IHJ. rewrite <- HJ. clear; firstorder. clear -Hf; firstorder. Qed.
imports: lset lattice ordinal