proposition: Lemma linear_reduce_aux : forall i p, valid (Pos.succ i) p -> linear i (reduce_aux i p).
proof: Proof. intros i p; revert i; induction p; intros i Hp; simpl. + constructor. + inversion Hp; subst; case_decide; subst. - rewrite <- (Pos.max_id i) at 1; apply poly_add_linear_compat. { apply IHp1; eapply valid_le_compat; [eassumption|lia]. } { intuition. } - case_decide. { apply IHp1; eapply valid_le_compat; [eauto|lia]. } { constructor; try lia; auto. erewrite (reduce_aux_le_compat p2); [|assumption|lia]. apply IHp1; eapply valid_le_compat; [eauto|]; lia. } Qed.
imports: Bool PArith DecidableClass Ring Lia