(n m : nat) : (m <= n)%nat -> (n - m)%int = (n - m)%nat :> Int. Proof. intros H. induction H as [|n H IHn]. - lhs nrapply int_add_neg_r. by rewrite nat_sub_cancel. - rewrite nat_sub_succ_l; only 2: exact _. rewrite <- 2 int_nat_succ. rewrite int_add_succ_l. exact (ap _ IHn). Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.