proposition: Lemma plus_minus_assoc : forall a b c : nat, b <= a -> a - b + c = a + c - b.
proof: Proof. simple induction c. repeat rewrite Nat.add_comm with (m := 0); simpl in |- *; auto with arith. intros n H0 H1; repeat rewrite <- plus_n_Sm. rewrite H0; auto with arith. Qed.
imports: Coq(Arith ArithRing)