proposition: Lemma max_const_Const_leq : forall t, Const_leq (max_const t) t.
proof: Proof. intros. induction t; try (constructor; simpl; lia); constructor; simpl; eapply Const_leq_trans; try eassumption; (try now apply PeanoNat.Nat.le_max_l); (try now apply PeanoNat.Nat.le_max_r); lia. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) String QuickChick(QuickChick) Arith List Lia QuickChick.stlc(lambda) Wellfounded