proposition: Lemma fixed_point_is_prefixed : forall a, fixed_point a -> prefixed_point a.
proof: Proof. unfold fixed_point, prefixed_point; intros. eapply PO.le_proper; eauto. apply PO.eq_refl. apply PreO.le_refl. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat