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