/3 width=1 by at_inv_total, at_basic_ge/ qed-.
(* Specific main properties on basic relocation *****************************)
theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
/3 width=1 by at_inv_total, at_basic_ge/ qed-.
(* Specific main properties on basic relocation *****************************)
theorem basic_swap: ∀d1,d2. d2 ≤ d1 →