proposition: Lemma transitive_option_cpo_aux : forall (x y: option A), option_cpo x y -> forall z, option_cpo y z -> option_cpo x z.
proof: Proof. intros x y H; inversion H; auto. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith