proposition: Lemma highest_var_descr (x:h10upc) : let hv := highest_var x in match x with ((a,b),(c,d)) => a <= hv /\ b <= hv /\ c <= hv /\ d <= hv end.
proof: Proof. destruct x as [[a b] [c d]]. cbn. repeat split; lia. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)