proposition: Lemma align_3_aux1: forall p1 p2 k1 k2, (p1 = k1 * 3 -> p2 = k2 * 3 -> p1 = p2 + 1 -> False)%nat.
proof: Proof. intros. subst. destruct (le_dec k1 k2). + pose proof mult_le_compat_r _ _ 3 l. lia. + assert (k2 * 3 < k1 * 3) by (apply Nat.mul_lt_mono_pos_r; lia). lia. 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