proposition: Lemma div_mul a b c : a / (b * c) = a / c / b.
proof: Proof. apply/le_anti/andP; split. - by rewrite -!mul_div_equiv -mulrA; apply: div_mul_le. - by rewrite -mul_div_equiv mulrA !mul_div_equiv; exact: lexx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice