proposition: Theorem sinc_decidable : (forall n, exists k, n <= k /\ P k) * (forall n, { P n } + { ~ P n }).
proof: Proof. Proof using HP Hf. split; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list utils_nat)