proposition: Theorem Nat_sub_sub_distr : ∀ n m p, (p ≤ m → n - (m - p) = n + p - m)%nat.
proof: Proof. intros n m p Hpm. rewrite Nat.add_comm. revert n m Hpm. induction p; intros. rewrite Nat.sub_0_r, Nat.add_0_l; reflexivity. destruct m as [| m]. exfalso; revert Hpm; apply Nat.nle_succ_0. rewrite Nat.sub_succ; simpl. apply Nat.succ_le_mono in Hpm. apply IHp; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz