fact: Fixpoint iterate (x: A) (acc: Acc gt x) (PRE: le x (F x)) {struct acc}: A := let x' := F x in match eq_dec x x' with | left E => x | right NE => iterate x' (iterate_acc x acc PRE NE) (iterate_le x PRE) end.
imports: Coq(Extraction ExtrOcamlBasic)