proposition: Lemma transitive_option_cpo : transitive option_cpo.
proof: Proof. intros x y z H1 H2 ; apply transitive_option_cpo_aux with y ; assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith