proposition: Lemma plus_nat_eq_plus_int : forall (n m:nat), (n+m)%nat = (n:int) + (m:int) :> int.
proof: Proof. Proof using. Transparent nat_to_Z. intros. unfold nat_to_Z. applys Nat2Z.inj_add. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)