proposition: Lemma poly_mul_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr -> valid (Pos.max kl kr) (poly_mul pl pr).
proof: Proof. intros kl kr pl pr Hl Hr; revert kr pr Hr. induction Hl; intros kr pr Hr; simpl. + apply poly_mul_cst_valid_compat; auto. apply (valid_le_compat kr); now auto. + apply (valid_le_compat (Pos.max (Pos.max i kr) (Pos.max (Pos.succ i) (Pos.max (Pos.succ i) kr)))). - case_decide. { apply (valid_le_compat (Pos.max i kr)); auto. } { apply poly_add_valid_compat; auto. now apply poly_mul_mon_valid_compat; intuition. } - repeat apply Pos.max_case_strong; lia. Qed.
imports: Bool PArith DecidableClass Ring Lia