proposition: Lemma is_order_bounded : Bounded.axioms is_order_on.
proof: Proof. ir. apply Bounded.little_criterion with (x -> x -> Prop) (fun lq : x -> x -> Prop => create x (little_leq lq)). ir. sh (lit_lq y). sy; ap create_little_leq. am. Qed.
imports: universe