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