proposition: Lemma invar_inv1 : forall n p : nat, invar (mkstate n p true) -> n0 = two_power p * n.
proof: Proof. intros; inversion_clear H; 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