proposition: Lemma abs_nonneg : forall (x:int), x >= 0 -> abs x = x :> int.
proof: Proof. Proof using. intros. rewrite inj_Zabs_nat. rewrite Z.abs_eq. math. math. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)