proposition: Fact list_One_Zero_inj a b l m : list_repeat One a ++ Zero :: l = list_repeat One b ++ Zero :: m -> a = b /\ l = m.
proof: Proof. revert b l m; induction a as [ | a IHa ]; intros [ | b ] l m; simpl; try discriminate. inversion 1; auto. intros H. inversion H as [ H1 ]. apply IHa in H1. destruct H1; subst; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)