proposition: Lemma abs_le_nat_le : forall (x:int) (y:nat), (0 <= x) -> (abs x <= y) = (x <= y)%Z.
proof: Proof. intros. extens. iff E. { rewrites~ <-(>> abs_to_int x). math. } { rewrites~ <-(>> abs_to_int x) in E. math. } Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)