proposition: Fact joinA : associative join.
proof: Proof. move=> x y z; rewrite /meet /min !(fun_if, if_arg). case: (leP z y) (leP y x) (leP z x) => [] zy [] yx [] zx//=. by have := le_lt_trans (le_trans zy yx) zx; rewrite ltxx. by apply/eqP; rewrite eq_le zx ltW// (lt_trans yx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)