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;
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;