proposition: Lemma poly_add_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr -> valid (Pos.max kl kr) (poly_add pl pr).
proof: Proof. intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl. { eapply valid_le_compat; [clear k|apply Pos.le_max_r]. now induction Hr; auto. } { assert (Hle : (Pos.max (Pos.succ i) kr <= Pos.max k kr)%positive) by auto. apply (valid_le_compat (Pos.max (Pos.succ i) kr)); [|assumption]. clear - IHHl1 IHHl2 Hl2 Hr H0; induction Hr. - constructor; auto. now rewrite <- (Pos.max_id i); intuition. - destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition. + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition. } Qed.
imports: Bool PArith DecidableClass Ring Lia