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