proposition: Lemma dsube_eq x y z : x \is a fin_num -> (y +? z) -> (x - z == y) = (x == y + z).
proof: Proof. by move: x y z => [x| |] [y| |] [z| |] // _ _; rewrite !eqe subr_eq. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed