proposition: Lemma le_total_order : Totally_ordered nat nat_po Integers.
proof: Proof. apply Totally_ordered_definition. simpl. intros H' x y H'0. elim Nat.le_gt_cases with (n := x) (m := y). - intro H'1; left; auto with sets arith. - intro H'1; right. apply Nat.lt_le_incl; assumption. 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