proposition: Lemma cl_sup_subset : forall (P P' : A -> Prop), (forall a, P a -> P' a) -> le (cl_sup P) (cl_sup P').
proof: Proof. intros. eapply (proj2 (sup_lub P)); intros. eapply (proj1 (sup_lub P')); eauto. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat