proposition: Theorem iterates_none_imp_fix_none : forall A B f, continuous (f_order A B)(f_order A B) f-> forall x, (forall n, iter _ f n (fun z => None) x = None) -> Tarski_fix f x = None.
proof: Proof. intros A B f Hct x Happr. case_eq (Tarski_fix f x). intros v Heq; destruct (Tarski_fix_iterates_witness A B f Hct x v Heq) as [n Heq']. rewrite (Happr n) in Heq'; discriminate. trivial. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith