proposition: Lemma chains_order: order chains_ord.
proof: Proof. constructor. - unfold reflexive, chains_ord. auto with sets. - unfold transitive, chains_ord. auto with sets. - intros [?] [?] ? ?. apply subset_eq_compat. auto with sets. Qed.
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients EnsemblesSpec