proposition: Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p.
proof: Proof. intros i p; induction p; simpl; case_decide; simpl; inversion 1; intuition. Qed.
imports: Bool PArith DecidableClass Ring Lia