proposition: Lemma sup_pointwise {A} {OA} {X : t A OA} {Ix Ix'} (f : Ix -> A) (g : Ix' -> A) : (forall (i : Ix), exists (j : Ix'), L.le (f i) (g j)) -> L.le (sup f) (sup g).
proof: Proof. intros. eapply PreO.sup_least. apply sup_ok. intros. destruct (H i). eapply PreO.le_trans. eassumption. apply PreO.sup_ge. apply sup_ok. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat