+lemma modularj: ∀R.∀L:vlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
+intros (R L y z);
+lapply (modular_mjp ?? y z) as H1;
+apply (plus_cancr ??? (μ(y ∧ z)));
+apply (eq_trans ?? ? ? H1); clear H1;
+apply (eq_trans ?? ? ?? (plus_assoc ????));
+apply (eq_trans ?? (μy+ μz + 0)); [2: apply feq_plusl; apply eq_sym; apply opp_inverse]
+apply (eq_trans ?? ? ?? (plus_comm ???));
+apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply eq_reflexive.
+qed.
+
+lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z).
+intros (R L y z);
+lapply (modular_mjp ?? y z) as H1;
+apply (plus_cancl ??? (μ(y ∨ z)));
+apply (eq_trans ?? ? ? H1); clear H1;
+apply (eq_trans ????? (plus_comm ???));
+apply (eq_trans ?? ? ?? (plus_assoc ????));
+apply (eq_trans ?? (μy+ μz + 0)); [2: apply feq_plusl; apply eq_sym; apply opp_inverse]
+apply (eq_trans ?? ? ?? (plus_comm ???));
+apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply eq_reflexive.
+qed.
+
+lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
+intros (R L x y z);
+lapply (modular_mjp ?? x (y ∨ z)) as H1;
+apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z)))); [2: apply feq_plusr; apply H1;] clear H1;
+apply (eq_trans ?? ? ?? (plus_comm ???));
+(* apply (eq_trans ?? (0+μ(x∧(y∧z))) ?? (opp_inverse ??)); ASSERT FALSE *)
+apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z)))); [2: apply eq_sym; apply plus_assoc;]
+apply (eq_trans ?? (0+μ(x∧(y∨z)))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse;]
+(* apply (eq_trans ?? ? ? (eq_refl ??) (zero_neutral ??)); ASSERT FALSE *)
+apply (eq_trans ?? (μ(x∧(y∨z)))); [apply eq_reflexive]
+apply eq_sym; apply zero_neutral.
+qed.
+
+lemma modularjm: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
+intros (R L x y z);
+lapply (modular_mjp ?? x (y ∧ z)) as H1;
+apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
+apply (eq_trans ?? ? ?? (plus_comm ???));
+apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z))); [2: apply eq_sym; apply plus_assoc]
+apply (eq_trans ?? (0+ μ(x∨y∧z))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse]
+apply eq_sym; apply zero_neutral;
+qed.
+
+lemma step1_3_57': ∀R.∀L:vlattice R.∀x,y,z:L.
+ μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)).
+intros (R L x y z);
+apply (eq_trans ?? ? ? (modularjm ?? x y z));
+apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [
+ apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);]
+apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
+ apply feq_plusl; apply feq_opp;
+ apply (eq_trans ?? ? ? (meet_assoc ?????));
+ apply (eq_trans ?? ? ? (meet_comm ????));
+ apply eq_reflexive;]
+apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply plus_assoc;
+qed.
+