proposition: Lemma plus_minus : forall n m r, r<=m -> (n+m)-r=n+(m-r).
proof: Proof. induction n. intros. simpl. reflexivity. intros. assert (S n+m=S(n+m)). auto with arith. rewrite H0. symmetry. rewrite Nat.sub_succ_l. rewrite IHn. auto with arith. exact H. assert (m<=n+m). auto with arith. apply Nat.le_trans with m. exact H. exact H1. Qed.
imports: Coq(Arith Lia)