proposition: Lemma eval_mkPX vs : forall P v Q, eval vs (mkPX P v Q) = (eval vs P) * (vs v) + eval vs Q.
proof: Proof. intros. unfold mkPX. rewrite eval_add,eval_mulX. reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings