proposition: Lemma gte_subl y x : y \is a fin_num -> (y - x < y) = (0 < x).
proof: Proof. move: y x => [x| |] [y| |] _ //; rewrite addeC /= ?ltNyr ?ltry//. by rewrite !lte_fin gtrDr ltrNl oppr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed