proposition: Lemma suffix_cons_inv l1 l2 x y : x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
proof: Proof. intros [[|? k] E]; [by left|]. right. simplify_eq/=. by apply suffix_app_r. Qed.
imports: stdpp(options)