proposition: Lemma fixpoint_smallest: forall z, le (F z) z -> le fixpoint z.
proof: Proof. intros z LEz. assert (REC: forall x acc PRE, le x z -> le (iterate x acc PRE) z). { induction x using (well_founded_induction gt_wf). intros. destruct acc; cbn. destruct (eq_dec x (F x)). - auto. - apply H. split; auto. apply le_trans with (F z). apply F_mon; auto. apply LEz. } apply REC. apply bot_smallest. Qed.
imports: Coq(Extraction ExtrOcamlBasic)