proposition: Theorem spec_2: forall p v', ( exp2 v' <= div2 (S (S p)) < 2 * exp2 v' ) -> ( exp2 (S v') <= S (S p) < 2 * exp2 (S v') ).
proof: Proof. intros p v' H; (cbv zeta iota beta delta [exp2]; fold exp2). elim (div2_eq (S (S p))); intros; lia. Qed.
imports: Arith ArithRing Lia log2_it