proposition: Lemma chains_ord_exists (x : chains) : (forall x:T, exists y:T, R x y /\ x <> y) -> exists y : chains, chains_ord x y /\ x <> y /\ (forall z : chains, chains_ord x z -> chains_ord z y -> z = x \/ z = y).
proof: Proof. intro H3. destruct x, (ub_of_chain x c), (H3 x0). pose (x' := Add x x1). assert (chain R x'). - red. intros. case H1. + case H2; intros. * now apply c. * destruct H4. left. apply ord_trans with x0; now apply H + destruct H0. + intros x3 []. destruct H2 as [? | ? []]. * right. apply ord_trans with x0; now apply H + destruct H0. * left. now apply ord_refl. - exists (exist _ x' H1). unfold chains_ord. repeat split; intros. + now constructor. + intuition. injection H2. intro. assert (In x x1) by (rewrite H0; now constructor 2). contradict H5. now apply (ord_antisym ord), H. + destruct z, (classic (In x2 x1)); [ right | left ]; apply subset_eq_compat, Extensionality_Ensembles; split; trivial; red; intros. * case H6; trivial. now intros ? []. * assert (In x' x3) by now apply H4. inversion H7; trivial. now destruct H8. Qed.
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients EnsemblesSpec