proposition: Lemma reduce_aux_le_compat : forall k l p, valid k p -> (k <= l)%positive -> reduce_aux l p = reduce_aux k p.
proof: Proof. intros k l p; revert k l; induction p; intros k l H Hle; simpl; auto. inversion H; subst; repeat case_decide; subst; try lia. + apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|lia]. + f_equal; apply IHp1; auto. now eapply valid_le_compat; [eauto|lia]. Qed.
imports: Bool PArith DecidableClass Ring Lia