proposition: Lemma dup_suffix_eq p q s1 s2 : s1~1~0 ++ dup p = s2~1~0 ++ dup q → p = q.
proof: Proof. revert q. induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=. - by rewrite (IH q). - by rewrite (IH q). - reflexivity. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)