X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=d6b637a0d35990479747b897ed5300b9e09dd0db;hb=3a5b9647787e1402f6886d41824f664db290963f;hp=46662b5881f8990bd9c4e7d77d482a265b993c8a;hpb=9d60f524ea49744e5339a3da981a7263ea92ace6;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 46662b588..d6b637a0d 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -55,4 +55,33 @@ intro l; apply (mk_excedence l (excl l));
   assumption]
 qed.    
 
-coercion cic:/matita/lattice/excedence_of_lattice.con.
\ No newline at end of file
+coercion cic:/matita/lattice/excedence_of_lattice.con.
+
+lemma feq_ml: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
+intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
+intro H1; apply H; clear H; apply (strong_extm ???? H1);
+qed.
+
+lemma feq_jl: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∨ a) ≈ (c ∨ b).
+intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
+intro H1; apply H; clear H; apply (strong_extj ???? H1);
+qed.
+
+lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b).
+intros (l a b H); 
+  unfold le in H; unfold excedence_of_lattice in H;
+  unfold excl in H; simplify in H; 
+unfold eq; assumption;
+qed.
+
+lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b).
+intros (l a b H); lapply (le_to_eqm ??? H) as H1;
+lapply (feq_jl ??? b H1) as H2;
+apply (Eq≈ ?? (join_comm ???));
+apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H;
+apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
+apply eq_sym; apply absorbjm;
+qed.
+
+
+