proposition: Lemma abs_eq_nat_eq : forall (x:int) (y:nat), x >= 0 -> (abs x = y :> nat) = (x = Z_of_nat y :> int).
proof: Proof. Proof using. introv M. extens. iff E. { subst. rewrite Zabs2Nat.id_abs, Z.abs_eq; math. } { subst. rewrite~ Zabs2Nat.id. } Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)