proposition: Lemma lcomparableP x y : incomparel x y (min y x) (min x y) (max y x) (max x y) (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).
proof: Proof. by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy; rewrite ?(meetxx, joinxx); rewrite ?(meet_l hxy', meet_r hxy', join_l hxy', join_r hxy'); constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)