proposition: Lemma minus_nat_eq_minus_int : forall (n m:nat), (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_sub. math. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)