proposition: Lemma lt0e x : (0 < x) = (x != 0) && (0 <= x).
proof: Proof. by case: x => [r| |]//; rewrite lte_fin lee_fin lt0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed