proposition: Lemma divAC : right_commutative (@div _ D).
proof: Proof. move=> a b c; apply/le_anti/andP; split; rewrite -!mul_div_equiv. - by rewrite -mulrA (mulrC b) mulrA !mul_div_equiv. - by rewrite -mulrA (mulrC c) mulrA !mul_div_equiv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice