proposition: Lemma align_3_aux: forall x, Z.divide 3 (Z.of_nat x) <-> exists k, x = (k * 3) % nat.
proof: Proof. intros. unfold Z.divide. split; intros [?k ?]. + exists (Z.to_nat k). rewrite <- (Nat2Z.id x). rewrite H. assert (0 <= k)%Z. 1: { destruct (Z_lt_le_dec k 0%Z); auto. assert (k * 3 < 0 * 3)%Z by (apply Z.mul_lt_mono_pos_r; lia). simpl in H0. lia. } apply Z2Nat.inj_mul; lia. + exists (Z.of_nat k). rewrite H. apply Nat2Z.inj_mul. Qed.
imports: CertiGraph.msl_application.Graph VST.msl.seplog VST.msl.log_normalize VST.msl.alg_seplog_direct CertiGraph.msl_ext.abs_addr CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.precise_direct CertiGraph.msl_ext.overlapping_direct CertiGraph.msl_ext.alg_seplog_direct CertiGraph.msl_ext.ramify_tactics CertiGraph.heap_model_direct.SeparationAlgebra CertiGraph.heap_model_direct.mapsto CertiGraph.heap_model_direct.SeparationLogic VST.msl.msl_direct VST.msl.predicates_sa Coq.Numbers.Natural.Peano.NPeano Coq.ZArith.Znumtheory