-
-(* Inversion lemmas with application ****************************************)
-
-lemma at_basic_inv_lt: ∀m,n,i,j. i < m → @❪i, 𝐁❨m,n❩❫ ≘ j → i = j.
-/3 width=4 by at_basic_lt, at_mono/ qed-.
-
-lemma at_basic_inv_ge: ∀m,n,i,j. m ≤ i → @❪i, 𝐁❨m,n❩❫ ≘ j → n+i = j.
-/3 width=4 by at_basic_ge, at_mono/ qed-.