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