proposition: Theorem value_upper_bound : forall f x, chain option_cpo f -> f x <> None -> upper_bound option_cpo (f x) f.
proof: Proof. intros f x Hchain Hneq y. case (le_gt_dec x y); [intros Hlexy | intros Hltyx]. assert (Hcpo: option_cpo (f x) (f y)) by (apply chain_le; auto). inversion Hcpo; [elim Hneq; auto | auto]. apply chain_le; auto with arith. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith