proposition: Lemma abs_minus : forall (x y:int), (x >= y) -> (y >= 0) -> abs (x - y) = (abs x - abs y)%nat :> nat.
proof: Proof. Proof using. intros. applys Zabs2Nat.inj_sub; math. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)