proposition: Lemma to_nat_plus : forall (x y:int), (x >= 0) -> (y >= 0) -> to_nat (x + y) = (to_nat x + to_nat y)%nat :> nat.
proof: Proof. Proof using. intros. apply~ Z2Nat.inj_add. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)