proposition: Lemma four_divided_tenth_pl_false: forall n i, (4 | n) -> (n | Ptrofs.unsigned i) -> Ptrofs.testbit i 1 = false.
proof: Proof. intros. unfold Ptrofs.testbit. inversion H. inversion H0. rewrite H2. subst. replace (x0 * (x * 4))%Z with (2 * (x * x0 * 2))%Z by lia. rewrite Z.double_bits. simpl. rewrite Zodd_mod, Z_mod_mult. unfold Zeq_bool; reflexivity. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List