proposition: Lemma pow2_inj m: (2 ^ m)%N = BinNat.N.to_nat (BinNat.N.pow (BinNums.Npos (BinNums.xO 1%AC)) (BinNat.N.of_nat m)).
proof: Proof. elim: m => [// | m IHm]. rewrite expnSr Nnat.Nat2N.inj_succ BinNat.N.pow_succ_r' Nnat.N2Nat.inj_mul PeanoNat.Nat.mul_comm. by apply: f_equal2. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)