Lemma natdiffplusdiff {a b c} : a ≥ b -> b ≥ c -> a-c = (a-b) + (b-c). Proof. intros r s. apply (natplusrcan _ _ c). rewrite natplusassoc. rewrite (minusplusnmm _ _ s). rewrite (minusplusnmm _ _ (istransnatleh s r)). exact (! minusplusnmm _ _ r). Defined.