proposition: Lemma h10upc_ind_not_less_0 : forall k, h10upc_ind k 0 0 0 -> False.
proof: Proof. enough (forall a b c d, h10upc_ind a b c d -> b = 0 -> c = 0 -> d = 0 -> False) as H. 1: intros k H1; apply (H k 0 0 0 H1); easy. intros a b c d H. unshelve eapply (h10upc_ind_ind (fun a b c d => b = 0 -> c = 0 -> d = 0 -> False) _ _ a b c d H); clear a b c d H. - intros a Hb Hc Hd. lia. - intros a b c d b' c' d' Hab'c'd' Eab'c'd' Hd'b'dd' Ed'b'dd' Hb'zbz Eb'zbz Hc'0c0 Ec'0c0 Hb Hc Hd; cbn in *; subst. apply Ec'0c0; easy. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)