proposition: Lemma meetUl : left_distributive gcdn lcmn.
proof: Proof. move=> [|m'] [|n'] [|p'] //=; rewrite ?lcmnn ?lcm0n ?lcmn0 ?gcd0n ?gcdn0//. - by rewrite gcdnC meetKU. - by rewrite lcmnC gcdnC meetKU. apply: eqn_from_log; rewrite ?(gcdn_gt0, lcmn_gt0)//= => p. by rewrite !(logn_gcd, logn_lcm) ?(gcdn_gt0, lcmn_gt0)// minn_maxl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)