proposition: Lemma maxBetaLe : forall (n : nat) (x : nat -> nat) (i : nat), i < n -> x i <= maxBeta n x.
proof: Proof. simple induction n. - intros x i H; elim (Nat.nlt_0_r _ H). - intros; simpl in |- *. assert (lein: i <= n0) by lia; rewrite Nat.lt_eq_cases in lein; destruct lein. + eapply Nat.le_trans; [now apply H | apply Nat.le_max_r]. + rewrite H1; apply Nat.le_max_l. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow