proposition: Lemma to_nat_neg : forall (x:int), x <= 0 -> to_nat x = 0%nat.
proof: Proof. Proof using. intros x H. destruct~ x. assert (Z.pos p = 0) as ->. { forwards: Zle_0_pos p. math. } reflexivity. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)