proposition: Theorem transitive_f_order : forall A B, transitive (f_order A B).
proof: Proof. intros; unfold f_order; apply transitive_lift; apply transitive_option_cpo. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith