proposition: Theorem dExpPrimEq: (Z_of_N (N.double (dExp b) + Npos (xO (P_of_succ_nat t))) =2*(dExp b)+2*t+2)%Z.
proof: Proof. cut (forall (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z). intros T; rewrite <- T. 2:intros;unfold Nplus. 2:case x0; auto with zarith. replace (Zpos (xO (P_of_succ_nat t))) with (2*t+2)%Z. unfold N.double; case (dExp b); auto with zarith. lia. Qed.
imports: Reals ZArith List PeanoNat Psatz