proposition: Theorem nat_le_diff {n m : ℕ} (p : n ≤ m) : ∑ (k : ℕ), n + k = m.
proof: Proof. exists (m - n). rewrite natpluscomm. exact (minusplusnmm _ _ p). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA