proposition: Lemma eval_addX vs : forall c (v:V) Q, eval vs (addX c v Q) = phi c * vs v + eval vs Q.
proof: Proof. intros. unfold addX. pose proof (decide_eqb_ok c 0) as E. destruct (c =? 0). - rewrite (fst E) by split. rewrite (preserves_0 (f:=phi)). rewrite mult_0_l,plus_0_l. split. - apply eval_addX'. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings