proposition: Lemma GreatestFixedPoint_ind (Inv : A) : (le Inv (f Inv)) -> le Inv (cl_sup postfixed_point).
proof: Proof. intros; destruct (sup_lub postfixed_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