proposition: Lemma reflexive_option_cpo : reflexive option_cpo.
proof: Proof. Proof option_cpo_refl. Hint Resolve option_cpo_refl option_cpo_none_bot reflexive_option_cpo : core. Lemma antisym_option_cpo : antisymmetric option_cpo. intros x y H; inversion H. intros H'; inversion H'; trivial. trivial. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith