proposition: Lemma linear_reduce : forall k p, valid k p -> linear k (reduce p).
proof: Proof. intros k p H; induction H; simpl. + now constructor. + case_decide. - eapply linear_le_compat; [eauto|lia]. - constructor; auto. apply linear_reduce_aux; auto. Qed.
imports: Bool PArith DecidableClass Ring Lia