proposition: Lemma abs_gt_minus_nat : forall (n:nat) (x:int), (x >= n)%Z -> abs (x - n)%Z = (abs x - n)%nat.
proof: Proof. Proof using. introv N. applys eq_nat_of_eq_int. rewrite minus_nat_eq_minus_int. do 2 (rewrite abs_nonneg; [|math]). auto. applys ge_nat_of_ge_int. rewrite abs_nonneg; math. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)