proposition: Lemma expn2n : (succn (succn (Zp_trunc (2^n)))) = (2^n)%N.
proof: Proof. apply Zp_cast. pose proof n_pos as n_pos. destruct n as [| k]. 1:{ inversion n_pos. } rewrite expnS. move: (PositiveExp2 k). unfold Positive in n_pos. intro Hpos. unfold Positive in Hpos. rewrite !mulSnr. change (0 * ?n ^ ?m)%N with 0%N. set (m := (2^ k)%N) in *. clearbody m. apply /ltP. move: Hpos => /ltP Hpos. apply PeanoNat.Nat.lt_sub_lt_add_l. move: Hpos. case m. 1:{ intro h. inversion h. } intro n'. auto. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition pkg_rhl Package Prelude) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)