proposition: Lemma le_Order : Order nat le.
proof: Proof. split; [exact le_reflexive | exact le_trans | exact le_antisym]. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image Infinite_sets Compare_dec Relations_1 Partial_Order Cpo