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.
+
+
+