diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index c858914cf5770893080595ccac047dbfb2e87a8b..23b220013c3707005fd624b4e96bc77f0176ff11 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -852,35 +852,35 @@ Qed.
 
 (** Distributivity. *)
 
-Lemma distrib_union_union_l :
+Lemma union_union_distr_l :
   forall (A B C : U -> Prop),
     union A (union B C) = union (union A B) (union A C).
 Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_union_union_r :
+Lemma union_union_distr_r :
   forall (A B C : U -> Prop),
     union (union A B) C = union (union A C) (union B C).
 Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_union_inter_l :
+Lemma union_inter_distr_l :
   forall (A B C : U -> Prop),
     union A (inter B C) = inter (union A B) (union A C).
 Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_union_inter_r :
+Lemma union_inter_distr_r :
   forall (A B C : U -> Prop),
     union (inter A B) C = inter (union A C) (union B C).
 Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_union_inter :
+Lemma union_inter :
   forall (A B C D : U -> Prop),
     union (inter A B) (inter C D) =
     inter (inter (union A C) (union B C)) (inter (union A D) (union B D)).
@@ -888,21 +888,21 @@ Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_inter_union_l :
+Lemma inter_union_distr_l :
   forall (A B C : U -> Prop),
     inter A (union B C) = union (inter A B) (inter A C).
 Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_inter_union_r :
+Lemma inter_union_distr_r :
   forall (A B C : U -> Prop),
     inter (union A B) C = union (inter A C) (inter B C).
 Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_inter_union :
+Lemma inter_union :
   forall (A B C D : U -> Prop),
     inter (union A B) (union C D) =
     union (union (inter A C) (inter B C)) (union (inter A D) (inter B D)).
@@ -910,14 +910,14 @@ Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_inter_inter_l :
+Lemma inter_inter_distr_l :
   forall (A B C : U -> Prop),
     inter A (inter B C) = inter (inter A B) (inter A C).
 Proof.
 intros; rewrite subset_ext_equiv; split; subset_auto.
 Qed.
 
-Lemma distrib_inter_inter_r :
+Lemma inter_inter_distr_r :
   forall (A B C : U -> Prop),
     inter (inter A B) C = inter (inter A C) (inter B C).
 Proof.
@@ -931,7 +931,7 @@ Proof.
 intros A B H1 H2 H3; rewrite disj_equiv_def in H1, H3.
 contradict H2; apply empty_emptyset.
 rewrite <- (inter_full_l B).
-rewrite <- (union_compl_l A), distrib_inter_union_r, H1, H3.
+rewrite <- (union_compl_l A), inter_union_distr_r, H1, H3.
 now apply empty_union.
 Qed.
 
@@ -1161,28 +1161,28 @@ Proof.
 intros; subset_ext_auto x.
 Qed.
 
-Lemma diff_union_l :
+Lemma diff_union_distr_l :
   forall (A B C : U -> Prop),
     diff (union A B) C = union (diff A C) (diff B C).
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma diff_union_r :
+Lemma diff_union_distr_r :
   forall (A B C : U -> Prop),
     diff A (union B C) = inter (diff A B) (diff A C).
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma diff_inter_l :
+Lemma diff_inter_distr_l :
   forall (A B C : U -> Prop),
     diff (inter A B) C = inter (diff A C) (diff B C).
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma diff_inter_r :
+Lemma diff_inter_distr_r :
   forall (A B C : U -> Prop),
     diff A (inter B C) = union (diff A B) (diff A C).
 Proof.
@@ -1231,14 +1231,14 @@ Proof.
 intros; subset_ext_auto x.
 Qed.
 
-Lemma distrib_inter_diff_l :
+Lemma inter_diff_distr_l :
   forall (A B C : U -> Prop),
     inter A (diff B C) = diff (inter A B) (inter A C).
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma distrib_inter_diff_r :
+Lemma inter_diff_distr_r :
   forall (A B C : U -> Prop),
     inter (diff A B) C = diff (inter A C) (inter B C).
 Proof.
@@ -1444,7 +1444,7 @@ Proof.
 intros; subset_ext_auto x.
 Qed.
 
-Lemma super_distrib_union_sym_diff_l :
+Lemma union_sym_diff_super_distr_l :
   forall (A B C : U -> Prop),
     incl (sym_diff (union A C) (union B C))
          (union (sym_diff A B) C).
@@ -1452,7 +1452,7 @@ Proof.
 intros; subset_auto.
 Qed.
 
-Lemma super_distrib_union_sym_diff_r :
+Lemma union_sym_diff_super_distr_r :
   forall (A B C : U -> Prop),
     incl (sym_diff (union A B) (union A C))
          (union A (sym_diff B C)).
@@ -1460,7 +1460,7 @@ Proof.
 intros; subset_auto.
 Qed.
 
-Lemma super_distrib_union_sym_diff :
+Lemma union_sym_diff_super_distr :
   forall (A B C D : U -> Prop),
     incl (sym_diff (union A C) (union B D))
          (union (sym_diff A B) (sym_diff C D)).
@@ -1468,7 +1468,7 @@ Proof.
 intros; subset_auto.
 Qed.
 
-Lemma sub_distrib_sym_diff_union_l :
+Lemma sym_diff_union_sub_distr_l :
   forall (A B C : U -> Prop),
     incl (sym_diff (union A B) C)
          (union (sym_diff A C) (sym_diff B C)).
@@ -1476,7 +1476,7 @@ Proof.
 intros; subset_auto.
 Qed.
 
-Lemma sub_distrib_sym_diff_union_r :
+Lemma sym_diff_union_sub_distr_r :
   forall (A B C : U -> Prop),
     incl (sym_diff A (union B C))
          (union (sym_diff A B) (sym_diff A C)).
@@ -1484,7 +1484,7 @@ Proof.
 intros; subset_auto.
 Qed.
 
-Lemma sub_distrib_sym_diff_union :
+Lemma sym_diff_union_sub_distr :
   forall (A B C D : U -> Prop),
     incl (sym_diff (union A B) (union C D))
          (union (sym_diff A C) (sym_diff B D)).
@@ -1495,21 +1495,21 @@ Qed.
 (* ((U -> Prop) -> Prop, sym_diff, inter) is a Boolean ring,
   ie an abelian ring with fullset as neutral for intersection. *)
 
-Lemma distrib_inter_sym_diff_l :
+Lemma inter_sym_diff_distr_l :
   forall (A B C : U -> Prop),
     inter (sym_diff A B) C = sym_diff (inter A C) (inter B C).
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma distrib_inter_sym_diff_r :
+Lemma inter_sym_diff_distr_r :
   forall (A B C : U -> Prop),
     inter A (sym_diff B C) = sym_diff (inter A B) (inter A C).
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma distrib_inter_sym_diff :
+Lemma inter_sym_diff_distr :
   forall (A B C D : U -> Prop),
     inter (sym_diff A B) (sym_diff C D) =
     sym_diff (sym_diff (inter A C) (inter A D))
@@ -1518,7 +1518,7 @@ Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma super_distrib_sym_diff_inter_l :
+Lemma sym_diff_inter_super_distr_l :
   forall (A B C : U -> Prop),
     incl (inter (sym_diff A C) (sym_diff B C))
          (sym_diff (inter A B) C).
@@ -1526,7 +1526,7 @@ Proof.
 intros; subset_auto.
 Qed.
 
-Lemma super_distrib_sym_diff_inter_r :
+Lemma sym_diff_inter_super_distr_r :
   forall (A B C : U -> Prop),
     incl (inter (sym_diff A B) (sym_diff A C))
          (sym_diff A (inter B C)).
@@ -1534,7 +1534,7 @@ Proof.
 intros; subset_auto.
 Qed.
 
-Lemma super_distrib_sym_diff_inter :
+Lemma sym_diff_inter_super_distr :
   forall (A B C D : U -> Prop),
     incl (inter (inter (sym_diff A C) (sym_diff A D))
                 (inter (sym_diff B C) (sym_diff B D)))
@@ -1631,7 +1631,7 @@ Lemma inter_partition_compat_l :
     partition A B C -> partition (inter D A) (inter D B) (inter D C).
 Proof.
 intros A B C D [H1 H2]; split.
-rewrite H1; apply distrib_inter_union_l.
+rewrite H1; apply inter_union_distr_l.
 now apply inter_disj_compat_l.
 Qed.