proposition: Lemma spec_mul_add_n1: forall n m x y z, let (q,r) := DoubleMul.double_mul_add_n1 ZnZ.zero ZnZ.WW ZnZ.OW (DoubleMul.w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c) (S m) x y z in ZnZ.to_Z q * (base (ZnZ.digits (nmake_op _ (dom_op n) (S m)))) + eval n (S m) r = eval n (S m) x * ZnZ.to_Z y + ZnZ.to_Z z.
proof: Proof. intros n m x y z. rewrite digits_nmake. unfold eval. rewrite nmake_double. apply DoubleMul.spec_double_mul_add_n1. apply ZnZ.spec_0. exact ZnZ.spec_WW. exact ZnZ.spec_OW. apply DoubleCyclic.spec_mul_add. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen