proposition: Lemma eval_mulX@{} vs : forall (v:V) (P:Pol), eval vs (mulX v P) = eval vs P * vs v.
proof: Proof. induction P as [c|P1 IH1 w P2 IH2]. - simpl. rewrite eval_addX. simpl. rewrite (preserves_0 (f:=phi)),plus_0_r. split. - simpl. pose proof (tricho_compare_eq v w) as E. destruct (v ?= w);[clear E|rewrite <-E by split;clear E w|clear E]. + simpl. rewrite plus_mult_distr_r,IH1,IH2. apply ap011;trivial. rewrite <-2!mult_assoc;apply ap,mult_comm. + simpl. rewrite (preserves_0 (f:=phi)),plus_0_r. reflexivity. + simpl. rewrite (preserves_0 (f:=phi)),plus_0_r. reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings