proposition: Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_cst v p).
proof: Proof. intros k v p H; induction H; simpl; [now auto|]. case_decide; [|now auto]. eapply (valid_le_compat i); [now auto|lia]. Qed.
imports: Bool PArith DecidableClass Ring Lia