proposition: Lemma poly_add_linear_compat : forall kl kr pl pr, linear kl pl -> linear kr pr -> linear (Pos.max kl kr) (poly_add pl pr).
proof: Proof. intros kl kr pl pr Hl; revert kr pr; induction Hl; intros kr pr Hr; simpl. + apply (linear_le_compat kr); [|apply Pos.max_case_strong; lia]. now induction Hr; constructor; auto. + apply (linear_le_compat (Pos.max kr (Pos.succ i))); [|now auto]. induction Hr; simpl. - constructor; auto. replace i with (Pos.max i i) by (apply Pos.max_id); intuition. - destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. } { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. } { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. } { apply (linear_le_compat (Pos.max i0 (Pos.succ i))); intuition. } { apply (linear_le_compat (Pos.max i (Pos.succ i0))); intuition. } Qed.
imports: Bool PArith DecidableClass Ring Lia