proposition: Lemma subr_eq x y z : (x - z == y) = (x == y + z).
proof: Proof. exact: can2_eq (subrK z) (addrK z) x y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)