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