proposition: Lemma minus4:forall (a b c d:nat), (d<=c<=b)-> (a+b)+(c-d)=(a+c)+(b-d).
proof: Proof. intros a b c0 d H. cut (((Z_of_nat a)+(Z_of_nat b))+((Z_of_nat c0)-(Z_of_nat d))= ((Z_of_nat a)+(Z_of_nat c0))+((Z_of_nat b)-(Z_of_nat d)))%Z. intro H0. 2:intuition. elim H. intros H1 H2. set (H3:=(inj_minus1 c0 d H1)). rewrite<- H3 in H0. cut (d<=b). 2:intuition. intro H4. set (H5:=(inj_minus1 b d H4)). rewrite<- H5 in H0. intuition. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid