fact: Definition Tarski_fix (A B:Type) (f:(A->option B)->A->option B) : A->option B := (epsilon (inhabits (fun x => None)) (fun phi => least_fixpoint (f_order A B) f phi)).
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith