...

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index e588fd2bc2273d91b1e4122697ec7c0d0717da3b..6b81ce60bf5b0d4e33280cd4cb3f7b596de045de 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -19,6 +19,7 @@ include "nat/minus.ma".
 
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" = "setoid eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -58,4 +59,21 @@ nlemma partition_splits_card:
   | #x; #x'; nnormalize in ⊢ (? → ? → %);
     nelim daemon
   ]
+nqed.
+
+(************** equivalence relations vs partitions **********************)
+
+ndefinition partition_of_compatible_equivalence_relation:
+ ∀A:setoid. compatible_equivalence_relation A → partition A.
+ #A; #R; napply mk_partition
+  [ napply (quotient ? R)
+  | napply Full_set
+  | #a; napply mk_qpowerclass
+     [ napply {x | R x a}
+     | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
+##| #x; #_; nnormalize; napply (ex_intro … x); napply conj; napply refl
+  | #x; #x'; #_; #_; nnormalize; *; #x''; *; #H1; #H2; napply (trans ?????? H2);
+    napply sym; nassumption
+  | nnormalize; napply conj
+     [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##]
 nqed.
\ No newline at end of file