proposition: Lemma tail_addmul_spec r n m : tail_addmul r n m = r + n * m.
proof: Proof. revert m r; induction n as [| n IH]; simpl; trivial; intros. rewrite IH, tail_add_spec. rewrite add_assoc. f_equal; apply add_comm. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass