proposition: Lemma LeastFixedPoint_ind (Inv : A) : (le (f Inv) Inv) -> le (cl_inf prefixed_point) Inv.
proof: Proof. intros; destruct (inf_glb prefixed_point) as [? ?]. eapply H0; simpl; intros. unfold prefixed_point; eauto. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat