proposition: Lemma highest_num_descr (env:nat -> nat) (n:nat) (m:nat) : m <= n -> env m <= highest_num env n.
proof: Proof. induction n as [|n IH]. - intros Hm. assert (m=0) as Hm0. 1:lia. cbn. rewrite Hm0. lia. - intros HmSn. cbn. destruct (Nat.eq_dec (S n) m) as [Heq|Hneq]. + rewrite <- Heq. lia. + assert (m <= n) as Hmn. 1:lia. specialize (IH Hmn). lia. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)