21lemma edge_diff_invariant {δ : ℤ} {p q : Pot M} 22 (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {a b : M.U} (h : M.R a b) :
proof body
Tactic-mode proof.
23 (p b - q b) = (p a - q a) := by 24 have harr : (p b - q b) - (p a - q a) = (p b - p a) - (q b - q a) := by ring 25 have hδ : (p b - p a) - (q b - q a) = δ - δ := by simp [hp h, hq h] 26 have : (p b - q b) - (p a - q a) = 0 := by simp [harr, hδ] 27 exact sub_eq_zero.mp this 28 29/-- The difference (p − q) is constant along any n‑step reach. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.