proposition: Lemma exp_prop : forall (k : nat) (n : nat) (H : Two[#][0]), Two[^]k[*]nexp IR (n + k) ([1][/] (Two:IR)[//]H)[=] nexp IR n ([1][/] (Two:IR)[//]H).
proof: Proof. intros. astepl ((zexp Two H k)[*](nexp IR (n + k) ([1][/] Two[//]H) )). stepl ((zexp Two H k)[*](zexp Two H (- (n + k)%nat))). astepr (zexp Two H (k + (- (n + k)%nat))). apply eq_symmetric. apply zexp_plus. astepl (zexp Two H (-n)). apply (zexp_inv_nexp IR Two H n). replace (- n)%Z with (k + - (n + k)%nat)%Z; auto with zarith. apply eq_reflexive. intros. auto with zarith. assert ((n + k)%Z = (n + k)%nat). symmetry. apply inj_plus. auto with zarith. apply mult_wd; auto. apply eq_reflexive. apply (zexp_inv_nexp IR Two H (n+k)). Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory