proposition: Lemma h10upc_inv (a b c d : nat) : h10upc_sem_direct ((a,S b),(c,d)) -> {c':nat & {d':nat & h10upc_sem_direct ((a,b),(c',d')) /\ S c' = c /\ d' + b + 1 = d}}.
proof: Proof. intros [Hl Hr]. exists (a + S b). exists (c2 b). repeat split. - lia. - apply c2_descr. - lia. - enough (2*(c2 b + b + 1) = d+d) by nia. rewrite <- Hr. cbn. rewrite Nat.mul_comm. cbn. symmetry. pose (c2_descr b) as Hb. nia. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)