proposition: Fact meetUl : @left_distributive T T meet join.
proof: Proof. pose leP x y := lcomparable_leP (comparableT x y). move=> x y z; case: (leP x z); case: (leP y z); case: (leP x y); case: (leP x z); case: (leP y z); case: (leP x y) => //= xy yz xz _ _ _; rewrite ?joinxx //. - by move: (le_lt_trans xz (lt_trans yz xy)); rewrite ltxx. - by move: (lt_le_trans xz (le_trans xy yz)); rewrite ltxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)