proposition: Lemma div_top x : 1%O / x = 1%O.
proof: Proof. apply/le_anti /andP; split; [|rewrite -mul_div_equiv]; exact: lex1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice