proposition: Lemma invar_inv2 : forall n p : nat, invar (mkstate n p false) -> two_power p * n < n0 /\ n0 < two_power p * S n.
proof: Proof. intros. inversion_clear H; split; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl Euclid shift Compare_dec imperative while two_power log2_spec