proposition: Lemma plus''_assoc : forall n p q, plus'' n (plus'' p q) = plus'' (plus'' n p) q.
proof: Proof. simple induction q. - reflexivity. - simpl. intros; rewrite plus''_S. simpl; repeat rewrite plus''_S; auto. Qed.
imports: Arith